scientific article

Publication date: 1981

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

development predicate transformers program correctness Dijkstra's weakest preconditions Hoare's partial correctness logic

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items (only showing first 100 items - show all)

A Gentzen system for conditional logic ⋮ Proof rules for recursive procedures ⋮ Quasi-boolean equivalence ⋮ Weakest pre-condition reasoning for Java programs with JML annotations ⋮ Non-deterministic expressions and predicate transformers ⋮ A relational division operator: The conjugate kernel ⋮ Correct translation of data parallel assignment onto array processors ⋮ Modularity and reusability in attribute grammars ⋮ Weakest preconditions for pure Prolog programs ⋮ Application of the trace assertion method to the specification, design, and verification of automaton programs ⋮ Synthesis of positive logic programs for checking a class of definitions with infinite quantification ⋮ A categorical treatment of pre- and post-conditions ⋮ The formal development of a parallel program performing LU-decomposition ⋮ S- and T-invariants in cyber net systems ⋮ On the longest increasing subsequence of a circular list ⋮ Formal specification of parallel SIMD execution ⋮ Implementing (nondeterministic) parallel assignments ⋮ Algorithmically broad languages for polynomial time and space ⋮ The formal specification of abstract data types and their implementation in Fortran 90 ⋮ Unification: A case-study in data refinement ⋮ Predicate transformers as power operations ⋮ A theory of nonmonotonic rule systems I ⋮ Why there is no general solution to the problem of software verification ⋮ Convergence: integrating termination and abort-freedom ⋮ A sharp proof rule for procedures in WP semantics ⋮ Verification conditions are code ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Generation of convex polygons with individual angular constraints ⋮ A calculus of refinements for program derivations ⋮ A logical framework for evolving software systems ⋮ The co-invariant generator: An aid in deriving loop bodies ⋮ An exercise in proving self-stabilization with a variant function ⋮ Finite generation of ambiguity in context-free languages ⋮ Datalogy - the Copenhagen tradition of computer science ⋮ Running programs backwards: The logical inversion of imperative computation ⋮ Reflexive transitive invariant relations: A basis for computing loop functions ⋮ An elementary and unified approach to program correctness ⋮ Optimal algorithms for generalized searching in sorted matrices ⋮ Fundamentals of reversible flowchart languages ⋮ CASOP: A fast algorithm for computing the \(n\)-ary composition of a binary associative operator ⋮ Structural operational semantics through context-dependent behaviour ⋮ Do-it-yourself type theory ⋮ Command algebras, recursion and program transformation ⋮ A versatile concept for the analysis of loops ⋮ The algebra of conditional logic ⋮ Refinement concepts formalised in higher order logic ⋮ Derivation of efficient parallel programs: An example from genetic sequence analysis ⋮ A first order logic for partial functions ⋮ Combining relational calculus and the Dijkstra-Gries method for deriving relational programs ⋮ Enabledness and termination in refinement algebra ⋮ Deriving dense linear algebra libraries ⋮ Applying relation algebra and RelView to solve problems on orders and lattices ⋮ Repetitions, known or unknown? ⋮ Determinization of inverted grammar programs via context-free expressions ⋮ Algorithm design through the optimization of reuse-based generation ⋮ Predicate transformers and higher-order programs ⋮ Term rewriting and Hoare logic -- Coded rewriting ⋮ Symbolic execution formally explained ⋮ Constructing a program with exceptions ⋮ Games and winning strategies ⋮ Weakest preconditions for progress ⋮ Alternative developments of cyclic-permutation algorithms ⋮ Calculating with procedure calls ⋮ Loop invariants in floating point algorithms ⋮ Random list permutations in place ⋮ Non-associative parallel prefix computation ⋮ Polynomial-time inverse computation for accumulative functions with multiple data traversals ⋮ Adas and the equational theory of if-then-else ⋮ Embedding mappings and splittings with applications ⋮ A problem reduction based approach to discrete optimization algorithm design ⋮ General correctness: A unification of partial and total correctness ⋮ A unified approach of program verification ⋮ Auxiliary variables in partial correctness programming logics ⋮ An axiomatic treatment of SIMD assignment ⋮ Fifty years of Hoare's logic ⋮ Differentiators and detectors ⋮ Provably correct derivation of algorithms using FermaT ⋮ Power structures ⋮ A proof rule for while loop in VDM ⋮ Program inversion in the refinement calculus ⋮ The derivation of a tighter bound for top-down skew heaps ⋮ Theories for mechanical proofs of imperative programs ⋮ Data types over multiple-valued logics ⋮ P-A logic - a compositional proof system for distributed programs ⋮ Formal derivation of graph algorithmic programs using partition-and-recur ⋮ Opportunistic algorithms for eliminating supersets ⋮ Synthetic programming ⋮ Mathematics for reasoning about loop functions ⋮ Programs as proofs: A synopsis ⋮ A logic covering undefinedness in program proofs ⋮ A presentation of the Fibonacci algorithm ⋮ Strongest invariant functions: Their use in the systematic analysis of while statements ⋮ Automatic differentiation of algorithms ⋮ Convergence of iteration systems ⋮ Verifying Whiley programs with Boogie ⋮ On the decomposition of sequences into ascending subsequences ⋮ Equivalence of the Gries and Martin proof rules for procedure calls ⋮ On the mechanical derivation of loop invariants ⋮ Program refinement in fair transition systems ⋮ Normal form approach to compiler design

This page was built for publication: