scientific article; zbMATH DE number 3974258

zbMATH Open0603.68009MaRDI QIDQ3740201FDOQ3740201

Authors: Jifeng He, Tony Hoare 

Publication date: 1986

Title of this publication is not available (Why is that?)

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

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)

Cited In (35)

• Relational calculus as a formal system
• Title not available (Why is that?)
• Title not available (Why is that?)
• Nondeterministic semantics of compound diagrams
• Dynamic logic with program specifications and its relational proof system
• Statement inversion and strongest postcondition
• Proof system for weakest prespecification
• The weakest prespecification
• Combining angels, demons and miracles in program specifications
• On the lattice of specifications: Applications to a specification methodology
• Weakest Preconditions for High-Level Programs
• Joining specification statements
• Relation-algebraic semantics
• Title not available (Why is that?)
• Weakest preconditions for pure Prolog programs
• Towards reasoning about Hoare relations
• Title not available (Why is that?)
• Title not available (Why is that?)
• The weakest specifunction
• Datatype-generic termination proofs
• A formal software development approach using refinement calculus
• Extensions of Lambek calculi
• Data refinement of predicate transformers
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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)