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)

Full work available at URL https://doi.org/10.1007/BF00289504

Mathematics Subject Classification ID

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

Cites work

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

Cited in

(35)

• SIMD language design using prescriptive semantics
• 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
• More comments on the programming language Pascal
• SEMANOL (73), a metalanguage for programming the semantics of programming languages
• A proof rule for multiple coroutine systems
• Language design methods based on semantic principles
• A note on the semantic definition of side effects
• 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
• Deriving correctness properties of compiled code
• Automatic program verification. I: A logical basis and its implementation
• The verification and synthesis of data structures
• Fifty years of Hoare's logic
• Reverse Hoare logic
• The use of hoare logic in the verification of horizontal microprograms
• Monitors with arrays of condition variables and proof rules handling local quantities
• scientific article; zbMATH DE number 3514943 (Why is no real title available?)
• A multilevel flow control statement
• Design and implementation of an efficient priority queue
• A note on files in pascal
• An axiomatic treatment of SIMD assignment
• Embedding universal computer arithmetic in higher programming languages
• Utilizing Hoare logic to strengthen testing for error detection in programs
• Tony Hoare: his path to the ACM Turing Award
• Expressiveness and the completeness of Hoare's logic
• The axiomatic semantics of programs based on Hoare's logic
• Generation of correctness conditions for imperative programs
• Verification conditions are code

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)