Checking Semantic Requirements of Generic Algorithms

Abstract. Algorithms in computer algebra lend themselves naturally to the software design method of generic programming in the sense of the C++ STL library [14]: They abstract over their concrete input domain in favour of the properties that the domain must have; when calling a generic algorithm, the instantiation domain must provide these proper-ties. We seek to design a language for generic programming; in particular, the compiler should be aware of the proof obligations associated with instantiation and should assist in proving them. Since properties will in general be formulated in a rich logic, we introduce symbolic adjectives as names for underlying formulae. The compiler then works on sets of adjectives as a representation for properties; relations between properties become declared implications between sets of adjectives. We present a concise prototypical language Saga (Signatures and Ad-jectives for Generic Algorithms) that embodies this design principle and demonstrate its applicability by example.