Automatic Generation of Functional Programs from CASL Specifications

In this paper, we present a code generator transforming a class of CASL specifications into O´Caml programs. This code generator is dedicated to rapid prototyping of CASL specifications especially in the area of geometric modeling where algebraic formalisms have been used since the last decade. A large class of constructive equational specifications is handled by this generator while insuring the correctness of generated O´Caml programs. In particular, CASL specifications with many interpretation models (i.e. incomplete) are automatically supplemented in order to produce a program that implements one of them. Underlying properties, such as termination, completeness and confluence hold when equations satisfy some syntactic criteria given in the paper.