On formalised computer programs

DOI10.1016/S0022-0000(70)80022-8zbMath0209.18704OpenAlexW2010927194MaRDI QIDQ2543556

Publication date: 1970

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0022-0000(70)80022-8

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items

Automaton semigroup models of programs ⋮ Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines ⋮ Minimality and deadlockness of multitape automata ⋮ Unnamed Item ⋮ Solution of the generalized minimization problem for two-tape automata with one fixed tape ⋮ First order data types and first order logic ⋮ Program schemes, recursion schemes, and formal languages ⋮ The logic-termal equivalence is polynomial-time decidable ⋮ John McCarthy (1927--2011) ⋮ Observations on the complexity of regular expression problems ⋮ The independence of control structures in abstract programming systems ⋮ An algorithm deciding functional equivalence in a new class of program schemes ⋮ Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism ⋮ The IO- and OI-hierarchies ⋮ A survey of state vectors ⋮ Programs as partial graphs. I: Flow equivalence and correctness ⋮ Equational Theories of Abnormal Termination Based on Kleene Algebra ⋮ Definability by programs in first-order structures ⋮ Program equivalence checking by two-tape automata ⋮ Computing on structures ⋮ Unnamed Item ⋮ Inference rules for proving the equivalence of recursive procedures ⋮ The functional dimension of inductive definitions ⋮ Computability of String Functions Over Algebraic Structures Armin Hemmerling ⋮ The equivalence problem of multidimensional multitape automata ⋮ Program schemata and the first-order decision problem ⋮ Program schemata as automata. I ⋮ Program schemata with polynomial bounded counters ⋮ Inference Rules for Proving the Equivalence of Recursive Procedures ⋮ Some applications of topology to program semantics ⋮ Program equivalence and context-free grammars ⋮ The computational complexity of program schemata ⋮ Formal system of definition of data sets as a high-level tool of data extraction ⋮ Function iteration logics and flowchart schemata ⋮ The applicability of program schema results to programs ⋮ Completeness results for the equivalence of recursive schemas ⋮ Finiteness is mu-ineffable ⋮ Effective proper procedures and universal classes of program schemata ⋮ An improvement on Valiant's decision procedure for equivalence of deterministic finite turn pushdown machines ⋮ Una classe di schemi ricorsivi non-deterministici paralleli ⋮ Äquivalente Transformationen für Flußdiagramme ⋮ Program transformations and algebraic semantics ⋮ Modifications of the program scheme model ⋮ Parallel operator schemata over variable arrays and the maximal parallelism problem ⋮ Monadic recursion schemes: The effect of constants ⋮ Execution traces and programming-language semantics ⋮ On the non-compactness of the class of program schemas ⋮ Equivalences on program schemes ⋮ On the computational complexity of dynamic slicing problems for program schemas ⋮ Subrecursive program schemata I P II. I: Undecidable equivalence problems. II: Decidable equivalence problems ⋮ On program schemata equivalence ⋮ Characterization of flowchartable recursions ⋮ On approximate and algebraic computability over the real numbers ⋮ On self-modifying programs ⋮ A view of computability on term algebras ⋮ \(L(A)=L(B)\)? decidability results from complete formal systems ⋮ The totality problem for program schemas ⋮ Equivalence of conservative, free, linear program schemas is decidable ⋮ Necessary and sufficient conditions for the universality of programming formalisms ⋮ On the Decidability of the Equivalence Problem for Monadic Recursive Programs ⋮ Some thoughts on computational models: from massive human computing to abstract state machines, and beyond

Cites Work