An axiomatic definition of the programming language Pascal

DOI10.1007/BF00289504MaRDI QIDQ2560721zbMATH OpenFDO

Authors Niklaus Wirth, Tony Hoare

Publication date 1974

Published in Acta Informatica (Search for Journal in Brave)

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Formal languages and automata (68Q45)

Cites work

• scientific article; zbMATH DE number 3421895 (Why is no real title available?)
• A note on the for statement
• An axiomatic basis for computer programming
• The design of a pascal compiler

Cited in

(33)

• Correctness and efficiency of pattern matching algorithms
• PASCAL in LCF: Semantics and examples of proof
• The clean termination of Pascal programs
• Design and implementation of an efficient priority queue
• The verification and synthesis of data structures
• Verification conditions are code
• Fifty years of Hoare's logic
• Expressiveness and the completeness of Hoare's logic
• An axiomatic treatment of SIMD assignment
• Monitors with arrays of condition variables and proof rules handling local quantities
• Embedding universal computer arithmetic in higher programming languages
• Design and correctness of a compiler for a non-procedural language
• SIMD language design using prescriptive semantics
• The formal definition of a real-time language
• Deriving correctness properties of compiled code
• A multilevel flow control statement
• Reverse Hoare logic
• scientific article; zbMATH DE number 3514943 (Why is no real title available?)
• Axiomatic semantics for escape statements
• Remarks on R. D. Tennent's Language design methods based on semantic principles: Algol 68, a language designed using semantic principles
• Data types, abstract data types and their specification problem
• Generation of correctness conditions for imperative programs
• SEMANOL (73), a metalanguage for programming the semantics of programming languages
• The axiomatic semantics of programs based on Hoare's logic
• Automatic program verification. I: A logical basis and its implementation
• Correctness of the compiling process based on axiomatic semantics
• Floyd's principle, correctness theories and program equivalence
• More comments on the programming language Pascal
• The use of hoare logic in the verification of horizontal microprograms
• 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

Describes a project that uses

Uses Software

• ALGOL 60

This page was built for publication: An axiomatic definition of the programming language Pascal

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2560721)