Proof rules for recursive procedures

DOI10.1007/BF01211249MaRDI QIDQ1329196zbMATH OpenOpenAlexFDO

Authors W. H. Hesselink

Publication date 29 June 1994

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

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

zbMATH Keywords

Pascal-like languagePascal-proceduresrecursive procedures

Mathematics Subject Classification ID

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

Recommendations

• A Structure-directed Total Correctness Proof Rule for Recursive Procedure Calls
• scientific article; zbMATH DE number 3888897
• Inference rules for proving the equivalence of recursive procedures
• Proving total correctness of recursive procedures
• scientific article; zbMATH DE number 3942997

Cites work

• A general proof rule for procedures in predicate transformer semantics
• Command algebras, recursion and program transformation
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• On-the-fly garbage collection for several mutators
• Programs, Recursion and Unbounded Choice
• Repetitions, known or unknown?
• The derivation of systolic computations

Cited in

(26)

• Pseudo-recursive procedures
• A polynomial determination of the most-recent property in Pascal-like programs
• A correctness proof of sorting by means of formal procedures
• A sharp proof rule for procedures in WP semantics
• A proof rule for while loop in VDM
• Predicate transformers for recursive procedures with local variables
• Calculating sharp adaptation rules.
• Safety and progress of recursive procedures
• An algebraic treatment of procedure refinement to support mechanical verification
• scientific article; zbMATH DE number 3888897 (Why is no real title available?)
• scientific article; zbMATH DE number 3846835 (Why is no real title available?)
• Termination assertions for recursive programs: Completeness and axiomatic definability
• Inference rules for proving the equivalence of recursive procedures
• scientific article; zbMATH DE number 3942997 (Why is no real title available?)
• scientific article; zbMATH DE number 4005583 (Why is no real title available?)
• scientific article; zbMATH DE number 1086721 (Why is no real title available?)
• Polynomial recursion analysis in Pascal like programs
• scientific article; zbMATH DE number 3892562 (Why is no real title available?)
• Programming Languages and Systems
• An Inductive Theorem on the Correctness of General Recursive Programs
• A partial correctness proof for programs with decided specification
• Calculating with procedure calls
• Frame rule for mutually recursive procedures manipulating pointers
• Proving total correctness of recursive procedures
• Proof obligations for blocks and procedures
• Inference rules for proving the equivalence of recursive procedures

This page was built for publication: Proof rules for recursive procedures

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