Using an algebraic specification language as theorem prover for computational reals
Lecturer
Norbert Preining
JAIST, Research Center for Software Verification, Japan
Place/Time
CCA 2015 Twelfth International Conference on Computability and Complexity in Analysis
2015-07-15, Tokyo, Japan.
Abstract
CafeOBJ is a many- and order-sorted algebraic specification language from the OBJ family, related to languages like Casl and Maude. CafeOBJ allows us to have both the specification and the verification in the same language. It is based on powerful logical foundations (order-sorted algebra, hidden algebra, and rewriting logic) with an executable semantics. It has been
used to specify and verify extensive systems (e.g., railway signal systems, e-commerce protocols, authentication protocols), but at the same time it functions equally well as theorem prover using the built-in rewrite engine.
On the other hand, provable properties of computations on reals are highly desirable, and computational models of the reals based on sound logical foundations with effective algorithm form a favorable approach. Computational models of the reals are wide, ranging from interval arithmetic to all kind of sequence approximations, in particular streams (signed digit streams etc). Representing streams in a formal framework requires extra caution, as streams are infinite objects. Typical approaches use coinductive definitions.
Stream processing is a specific case of behavioral rewrite systems, and thus can be implemented in CafeOBJ, which provides hidden sorts allowing us to specify infinite data objects via a behavioral, i.e. coinductive, approach.
Aim of this work is a re-interpretation of CafeOBJ’s ‘specification’ part to provide an ‘implementation’ of exact reals, and its ‘verification’ part to prove properties of the exact reals.
Verification is realized by an executable semantics based on order-sorted rewriting. Using this approach, we provide the implementation, as well as its the verification of adequateness, as well as proofs of properties, all in the same framework of CafeOBJ.
After giving a short introduction to CafeOBJ and its syntax and semantical background, we will touch upon three areas related to exact real representation: (1) Extension of the number tower of CafeOBJ; (2) implement modules for the exact representation of reals; (3) use this representation to prove some simple lemmas.