Proving properties of Pascal programs in MIZAR 2

Reviewer: Kamal Lodaya

There is an old idea due to Burstall [1] to specify the semantics of a programming language using first-order predicates over state vectors (including control and data) and a transition relation. For example, the meaning of 1 : goto 2 is expressed by the axiom, ( Cs, s) ( sRs & control( s) = 1 :.BD( Cs, s) ( sRs:2WN control( s) = :- C2 & data( s) = data( s)). This can be reformulated in terms of sequences of states as ( Ch) ( control( state( h)) = 1 :.BD( Ch) control:2WN control( state( next( h)))- = 2 :.BD( Ch) control:2WN& data( state( next( h))) =- data( state( h))). Using basic notions such as value, address, etc., it is not surprising that the technique can be applied to Pascal data types, such as pointers and records, and all the Pascal control structures. Because the axioms are so low-level, general program properties can be proved, and since sequences are being considered, the properties need not be restricted to input-output relations (see also [2]). The authors translate programs written in a Pascal subset to axiomatic descriptions in a syntactically sugared version of first-order predicate calculus called MIZAR 2. Proofs in MIZAR 2 can now be verified using a proof checker. The paper describes this language and proves properties of a factorial and a list reversal program. It will be of slight interest to researchers in program verification. There is an extraordinary botch-up in the last section of the paper, where six figures seem to be missing. Moreover, there is a “comment on appendices” without any appendices being provided. Clearly, an explanation is called for from the authors and (especially) the editors of the journal.