Programs, Recursion and Unbounded Choice

DOI10.1017/CBO9780511569784MaRDI QIDQ4023579zbMATH OpenOpenAlexFDO

Authors W. H. Hesselink

Publication date 23 January 1993

Full work available at URL https://doi.org/10.1017/cbo9780511569784

zbMATH Keywords

semanticsweakest preconditionsequential programspredicate transformationformal specification and verification methodsunbounded choice

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Recommendations

• Predicate-transformer semantics of general recursion
• Recursive programs and denotational semantics in absolute logics of programs
• scientific article; zbMATH DE number 4123706
• scientific article; zbMATH DE number 4164150
• Predicate transformers and higher-order programs
• scientific article; zbMATH DE number 3924117
• scientific article; zbMATH DE number 194642
• scientific article; zbMATH DE number 176531
• scientific article; zbMATH DE number 1948157
• Infinite unfolding and transformations of nondeterministic programs

Cited in

(18)

• Lazy Relations
• Multirelations with infinite computations
• UNITY and Büchi automata
• Nondeterminacy and recursion via stacks and games
• Completeness of fair ASM refinement
• Simulation refinement for concurrency verification
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• Partial correctness for probabilistic demonic programs
• scientific article; zbMATH DE number 192929 (Why is no real title available?)
• Safety and progress of recursive procedures
• Normal design algebra
• Fixpoint semantics and simulation
• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• Proof rules for recursive procedures
• Repetitions, known or unknown?
• Syntactic translations and provably recursive functions
• Completeness of ASM refinement
• Set-theoretic models of computations

This page was built for publication: Programs, Recursion and Unbounded Choice

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