Proof obligations for blocks and procedures

DOI10.1007/BF01888232zbMath0707.68056MaRDI QIDQ919838

Alain Ah-kee

Publication date: 1990

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

AliasingOperation decomposition proofPost-conditionsstatic scoping

Mathematics Subject Classification ID

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

Related Items

Proof obligations for blocks and procedures

Uses Software

• Ada95
• ALGOL 60

Cites Work

• A logic covering undefinedness in program proofs
• Proof obligations for blocks and procedures
• Procedures, parameters, and abstraction: Separate concerns
• Revised report on the algorithmic language ALGOL 60
• A language of specified programs
• Side effects and aliasing can have simple axiomatic descriptions
• Assignment and Procedure Call Proof Rules
• Ten Years of Hoare's Logic: A Survey—Part I
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item