A language of specified programs (Q2265800)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A language of specified programs |
scientific article |
Statements
A language of specified programs (English)
0 references
1985
0 references
We 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.
0 references
specified programs
0 references
correctness
0 references