scientific article; zbMATH DE number 3974258

MaRDI QIDQ3740201zbMATH OpenFDO

Authors Jifeng He, Tony Hoare

Publication date 1986

zbMATH Keywords

formal methodssoftware engineeringprogram developmentgeneral recursionweakest prespecificationDijkstra's calculus of weakest preconditions

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

(35)

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

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)