Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II

DOI10.1016/S0304-3975(81)80001-1zbMath0461.68015MaRDI QIDQ1152704

Jean H. Gallier

Publication date: 1981

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

correctnesssemanticsrecursive proceduressecond-order predicate calculusnondeterministic flowchart programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items (6)

Equivalences and transformations of regular systems - applications to recursive program schemes and grammars ⋮ Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming ⋮ Semantics of algorithmic languages ⋮ Algebraic characterization of reducible flowcharts ⋮ Correctness of recursive parallel nondeterministic flow programs ⋮ Deterministic and nondeterministic flowchart interpretations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
• Theory of program structures: Schemes, semantics, verification
• On the completeness of the inductive assertion method
• First-order dynamic logic
• Automatic program verification. I: A logical basis and its implementation
• The correctness of nondeterministic programs
• Mathematical theory of partial correctness
• Completeness with Finite Systems of Intermediate Assertions for Recursive Program Schemes
• Is “sometime” sometimes better than “always”?
• Nondeterministic Algorithms
• Formalization of Properties of Functional Programs

This page was built for publication: Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II