Correctness of programs with Pascal-like procedures without global variables

DOI10.1016/0304-3975(84)90066-5zbMath0534.68016OpenAlexW2026086747MaRDI QIDQ790607

Ernst-Ruediger Olderog

Publication date: 1984

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(84)90066-5

zbMATH Keywords

expressivenessHoare-like systemsecond-order theory

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Reasoning about procedures as parameters in the language L4

Uses Software

• ALGOL 68

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The formal termination problem for programs with finite ALGOL 68-modes
• Sound and complete Hoare-like calculi based on copy rules
• The IO- and OI-hierarchies
• On termination problems for finitely interpreted ALGOL-like programs
• A sound and relatively* complete Hoare-logic for a language with higher type procedures
• Pascal. User manual and report. 2nd ed
• First-order dynamic logic
• On the notion of expressiveness and the rule of adaptation
• On correct procedure parameter transmission in higher programming languages
• Effective Axiomatizations of Hoare Logics
• Ten Years of Hoare's Logic: A Survey—Part I
• Generic commands--a tool for partial correctness formalisms
• Soundness and Completeness of an Axiom System for Program Verification
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• An axiomatic basis for computer programming