A language of specified programs (Q2265800): Difference between revisions
From MaRDI portal
Created a new Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 10:30, 2 February 2024
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