A language of specified programs (Q2265800): Difference between revisions
From MaRDI portal
Created a new Item |
Set OpenAlex properties. |
||
| (2 intermediate revisions by 2 users not shown) | |||
| Property / MaRDI profile type | |||
| Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1016/0167-6423(85)90004-8 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2005958325 / rank | |||
Normal rank | |||
| links / mardi / name | links / mardi / name | ||
Latest revision as of 21:04, 19 March 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
