Formulas as programs

Abstract

Alma-0 is a programming language supporting declarative programming, which combines the advantages of imperative and logic programming paradigms. This work explores declarative programming by extending the interpretation of Alma-0 programs to recursive and/or non-recursive procedures which exclude destructive assignments, and gives formal proofs for the implication: Implementation --> Specification for some non-trivial examples, e.g., finding a maximum element and various sorting algorithms.