Programs as partial graphs. I: Flow equivalence and correctness

DOI10.1016/0304-3975(81)90060-8zbMath0493.68015OpenAlexW2071945201WikidataQ127436288 ScholiaQ127436288MaRDI QIDQ1168723

Gunther Schmidt

Publication date: 1981

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

Full work available at URL: https://doi.org/10.1016/0304-3975(81)90060-8

zbMATH Keywords

correctnessterminationprogram semanticsprograms as partial graphs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (17)

Bjarni Jónsson's contributions in algebra ⋮ Relational algebraic semantics of deterministic and nondeterministic programs ⋮ A relational division operator: The conjugate kernel ⋮ Cryptomorphic topological structures: a computational, relation-algebraic approach ⋮ Relation-algebraic semantics ⋮ Parallel constructions of maximal path sets and applications to short superstrings ⋮ Partiality. II: Constructed relation algebras ⋮ Gunther Schmidt's life as a mathematician and computer scientist ⋮ Relational computation of sets of relations ⋮ Programs as partial graphs. II: Recursion ⋮ Discrete ordering relations ⋮ Relation algebraic domain constructions ⋮ Embedding a demonic semilattice in a relation algebra ⋮ Cardinality of relations with applications ⋮ Relation algebras: Concept of points and representability ⋮ Nondeterministic semantics of compound diagrams ⋮ Partiality. I: Embedding relation algebras

Cites Work

• The representation of relation algebras. II
• Programs as partial graphs. II: Recursion
• On the completeness of the inductive assertion method
• On the algebraic structure of rooted trees
• On homomorphisms, correctness, termination, unfoldments, and equivalence of flow diagram programs
• On formalised computer programs
• The representation of relational algebras
• On matrix program schemes
• Decidable Properties of Monadic Functional Schemas
• Guarded commands, nondeterminacy and formal derivation of programs
• Some Properties of Predicate Transformers
• Proving Properties of Programs by Structural Induction
• An axiomatic basis for computer programming
• Properties of Programs and the First-Order Predicate Calculus
• Formalization of Properties of Functional Programs
• Relations binaires, fermetures, correspondances de Galois
• Boolean Algebras with Operators. Part I
• Boolean Algebras with Operators
• 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

This page was built for publication: Programs as partial graphs. I: Flow equivalence and correctness