Assignment and Procedure Call Proof Rules

DOI10.1145/357114.357119MaRDI QIDQ3922131zbMATH OpenOpenAlexFDO

Authors David Gries, Gary Levin

Publication date 1980

Published in ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/357114.357119

zbMATH Keywords

axiomatic semanticsformal semanticsmultiple assignment

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited in

(12)

• An algebraic approach to the syntax and semantics of languages with subscripted variables
• A sharp proof rule for procedures in WP semantics
• A proof technique for communicating sequential processes
• Calculating sharp adaptation rules.
• On the notion of expressiveness and the rule of adaptation
• Secure mechanical verification of mutually recursive procedures
• Fifty years of Hoare's logic
• Mechanical verification of mutually recursive procedures
• A logical analysis of aliasing in imperative higher-order functions
• Inference rules for programming languages with side effects in expressions
• Semantical analysis of specification logic
• Proof obligations for blocks and procedures

This page was built for publication: Assignment and Procedure Call Proof Rules

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