Theory of program structures: Schemes, semantics, verification

zbMath0345.68002MaRDI QIDQ1233308

Sheila A. Greibach

Publication date: 1975

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01)

Related Items (47)

Continuation semantics for flowgraph equations ⋮ On flowchart theories. I. The deterministic case ⋮ Concurrent program schemes and their logics ⋮ Normal design algebra ⋮ On the detection of unstructuredness in flowgraphs ⋮ Succinct representation of regular sets using gotos and Boolean variables ⋮ Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming ⋮ Unnamed Item ⋮ A formal specification of document processing ⋮ On schematological equivalence of partially interpreted dataflow networks ⋮ Equivalence of linear, free, liberal, structured program schemas is decidable in polynomial time ⋮ Decision problems for pushdown threads ⋮ First order data types and first order logic ⋮ Recursion versus tail recursion over \(\overline{\mathbb{F}}_p\) ⋮ Program schemata vs. automata for decidability of program logics ⋮ Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. I ⋮ Read/write factorizable programs ⋮ Decidability of strong equivalence for subschemas of a class of linear, free, near-liberal program schemas ⋮ The equivalence of r.e. program schemes and data flow schemes ⋮ Computable queries for relational data bases ⋮ Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II ⋮ Methods and means of parallel processing of information ⋮ Recursion-closed algebraic theories ⋮ Floyd's principle, correctness theories and program equivalence ⋮ Deciding freeness for program schemes with a single unary function ⋮ Expressing program looping in regular dynamic logic ⋮ Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs ⋮ Unnamed Item ⋮ Characterizing minimal semantics-preserving slices of predicate-linear, free, liberal program schemas ⋮ Hoare's logic and Peano's arithmetic ⋮ Unnamed Item ⋮ A difference in complexity between recursion and tail recursion ⋮ Extended linear macro grammars, iteration grammars, and register programs ⋮ Modifications of the program scheme model ⋮ Propositional dynamic logic of regular programs ⋮ Monadic recursion schemes: The effect of constants ⋮ An analysis of the effect of rounding errors on the flow of control in numerical processes ⋮ Semantics of algorithmic languages ⋮ Expressive power of typed and type-free programming languages ⋮ On abstraction and the expressive power of programming languages ⋮ Two theorems about the completeness of Hoare's logic ⋮ Deterministic and nondeterministic flowchart interpretations ⋮ Equivalence of conservative, free, linear program schemas is decidable ⋮ Expressiveness and the completeness of Hoare's logic ⋮ The propositional dynamic logic of deterministic, well-structured programs ⋮ Equivalences among logics of programs ⋮ The unwind property for programs with bounded memory

This page was built for publication: Theory of program structures: Schemes, semantics, verification