A language of specified programs
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.
- Inductive assertion method for logic pograms
- Specifications, programs, and total correctness
- Multilevel structured program designs and correctness proving
- Exploring an interface model for CKA
- Developments in concurrent Kleene algebra
- scientific article; zbMATH DE number 3165828 (Why is no real title available?)
- Correct and Robust Programs
- A complete proof for the correctness of programs with new specification language
- Proving systolic systems correct
- scientific article; zbMATH DE number 4005581 (Why is no real title available?)
- scientific article; zbMATH DE number 550329 (Why is no real title available?)
- Probabilistic rely-guarantee calculus
- Convolution as a Unifying Concept
- A partial correctness proof for programs with decided specification
- Proof obligations for blocks and procedures
This page was built for publication: A language of specified programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2265800)
