An axiomatic definition of the programming language Pascal
From MaRDI portal
Publication:2560721
DOI10.1007/BF00289504zbMath0261.68040MaRDI QIDQ2560721
Publication date: 1974
Published in: Acta Informatica (Search for Journal in Brave)
Related Items
Unnamed Item, Generation of correctness conditions for imperative programs, Verification conditions are code, SIMD language design using prescriptive semantics, Embedding universal computer arithmetic in higher programming languages, The use of hoare logic in the verification of horizontal microprograms, Remarks on R. D. Tennent's Language design methods based on semantic principles: Algol 68, a language designed using semantic principles, Correctness of the compiling process based on axiomatic semantics, The formal definition of a real-time language, Floyd's principle, correctness theories and program equivalence, Axiomatic semantics for escape statements, Correctness and efficiency of pattern matching algorithms, A multilevel flow control statement, More comments on the programming language Pascal, SEMANOL (73), a metalanguage for programming the semantics of programming languages, Design and implementation of an efficient priority queue, A note on files in pascal, A proof rule for multiple coroutine systems, Language design methods based on semantic principles, A note on the semantic definition of side effects, Monitors with arrays of condition variables and proof rules handling local quantities, An axiomatic treatment of SIMD assignment, Fifty years of Hoare's logic, Design and correctness of a compiler for a non-procedural language, PASCAL in LCF: Semantics and examples of proof, Data types, abstract data types and their specification problem, The clean termination of Pascal programs, Reverse Hoare Logic, Automatic program verification. I: A logical basis and its implementation, The verification and synthesis of data structures, Deriving correctness properties of compiled code, Expressiveness and the completeness of Hoare's logic, The axiomatic semantics of programs based on Hoare's logic
Uses Software
Cites Work
