A language of specified programs

AbstractWe describe a language of specified programs devised to form a basis for a system for the development of provably-correct programs. A specified program, as introduced by Blikle and then developed in this paper, consists of statements and declarations (in our language these are standard sequential, conditional and loop statements, blocks with local variables and possibly recursive procedures and functions) interleaved with local assertions sufficient to prove the global correctness of the program. This requirement forces us to adopt the philosophy that all the properties of program objects we use in our programs must be explicitly stated in specifications