scientific article; zbMATH DE number 3974258

MaRDI QIDQ3740201zbMATH OpenFDO

Authors Jifeng He, Tony Hoare

Publication date 1986

zbMATH Keywords

Dijkstra's calculus of weakest preconditionsformal methodsgeneral recursionprogram developmentsoftware engineeringweakest prespecification

Mathematics Subject Classification ID

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

Recommendations

• The weakest prespecification
• Proof system for weakest prespecification
• scientific article; zbMATH DE number 512961
• scientific article; zbMATH DE number 3917681
• The weakest precondition calculus: Recursion and duality

Cited in

(38)

• Datatype-generic termination proofs
• The weakest prespecification
• Proof system for weakest prespecification
• Data refinement of predicate transformers
• Combining angels, demons and miracles in program specifications
• On the lattice of specifications: Applications to a specification methodology
• Statement inversion and strongest postcondition
• Protective interface specifications
• Joining specification statements
• The weakest precondition calculus: Recursion and duality
• Relation-algebraic semantics
• Parallel constructions of maximal path sets and applications to short superstrings
• Towards reasoning about Hoare relations
• The weakest specifunction
• Nondeterministic semantics of compound diagrams
• Weakest preconditions for pure Prolog programs
• Generalised rely-guarantee concurrency: an algebraic foundation
• Weakest Preconditions for High-Level Programs
• scientific article; zbMATH DE number 3917681 (Why is no real title available?)
• scientific article; zbMATH DE number 4020448 (Why is no real title available?)
• scientific article; zbMATH DE number 4022610 (Why is no real title available?)
• scientific article; zbMATH DE number 4047056 (Why is no real title available?)
• scientific article; zbMATH DE number 4068837 (Why is no real title available?)
• The Weakest Libera! Preconditions of Nondeterministic Machines and Robust Programs
• A Weakest Precondition Semantics for Z
• A Labelled Deductive System for Relational Semantics of the Lambek Calculus
• Dynamic logic with program specifications and its relational proof system
• scientific article; zbMATH DE number 1927431 (Why is no real title available?)
• scientific article; zbMATH DE number 1531358 (Why is no real title available?)
• Extensions of Lambek calculi
• RALL: machine-supported proofs for relation algebra
• A formal software development approach using refinement calculus
• Jifeng He at Oxford and beyond: an appreciation
• Relational calculus as a formal system
• Algebraic proofs of consistency and completeness
• Diagrammatic algebra of first order logic
• When Lawvere meets Peirce: an equational presentation of Boolean hyperdoctrines
• Infinitary action logic: complexity, models and grammars

This page was built for publication:

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