Programming as a Discipline of Mathematical Nature

From MaRDI portal
Publication:4773988

DOI10.2307/2319209zbMath0286.00013OpenAlexW4210314035WikidataQ56047772 ScholiaQ56047772MaRDI QIDQ4773988

Edsger W. Dijkstra

Publication date: 1974

Published in: The American Mathematical Monthly (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2319209



Related Items

Extending separation logic with fixpoints and postponed substitution, A recursion theorem for predicate transformers on inductive data types, A theory for nondeterminism, parallelism, communication, and concurrency, Comments on Morris's starvation-free solution to the mutual exclusion problem, A generalized deadlock predicate, A complete rule for equifair termination, Kleene's three-valued logic and process algebra, Weakest preconditions for pure Prolog programs, Efficient weakest preconditions, An efficient solution to the mutual exclusion problem using weak semaphores, A categorical treatment of pre- and post-conditions, Normal design algebra, Formal specification of parallel SIMD execution, Procedures and atomicity refinement, The formal specification of abstract data types and their implementation in Fortran 90, Creol: A type-safe object-oriented model for distributed concurrent systems, Deadlock and fairness in morphisms of transition systems, Online belief tracking using regression for contingent planning, Generation of convex polygons with individual angular constraints, An infinite pebble game and applications, Semantics of higher-order quantum computation via geometry of interaction, Parallel constructions of maximal path sets and applications to short superstrings, Universality and semicomputability for nondeterministic programming languages over abstract algebras, Auxiliary variables in data refinement, Interpretations of recursion under unbounded nondeterminacy, Space-efficient planar convex hull algorithms, The structured complexity of object-oriented programs, Mechanical inference of invariants for FOR-loops, Abstract representation theorems for demonic refinement algebras, Imperative abstractions for functional actions, A near-optimal method for reasoning about action, Generic weakest precondition semantics from monads enriched with order, Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic, Semantics of nondeterminism, concurrency, and communication, On limits and colimits of variety-based topological systems, On the total correctness of nondeterministic programs, Synthesising recursive functions with side effects, Transformational semantics for concurrent programs, Interweaving algebra and topology: lattice-valued topological systems, Computing Fibonacci numbers (and similarly defined functions) in log time, On correct refinement of programs, Floyd's principle, correctness theories and program equivalence, A transformational characterization of if-then-else, A versatile concept for the analysis of loops, Specifications, models, and implementations of data abstractions, A unified approach for studying the properties of transition systems, A model of reconfiguration in communicating sequential processes, A fuzzy language., A continuous semantics for unbounded nondeterminism, Domain theory in logical form, Correctness of concurrent processes, Data refinement of predicate transformers, Unifying wp and wlp, Duality beyond sober spaces: Topological spaces and observation frames, Constraint preservation through loops, Predicate transformers and higher-order programs, Algebraic proofs of consistency and completeness, Embedding a demonic semilattice in a relation algebra, Formalizing Dijkstra's predicate transformer wp in weak second-order logic, Computable concurrent processes, Constructing a program with exceptions, A sheaf-theoretic approach to pattern matching and related problems, Complete proof rules for strong fairness and strong extreme fairness, Combining angels, demons and miracles in program specifications, On the discretization in time for a parabolic integrodifferential equation with a weakly singular kernel. I: Smooth initial data, Finite-state concurrent programs can be expressed succinctly in triple normal form, A sketch of a dynamic epistemic semiring, An execution mechanism for nondeterministic, state-oriented programs based on a chart parser, Normal forms in total correctness for while programs and action systems, Turing machines, transition systems, and interaction, Alternating states for dual nondeterminism in imperative programming, A new look at the automatic synthesis of linear ranking functions, Improving multikey Quicksort for sorting strings with many equal elements, Prespecification in data refinement, A case for a forward predicate transformer, Glance: A lightweight querying service for wireless sensor networks, A starvation-free solution to the mutual exclusion problem, HasCasl: integrated higher-order specification and program development, Program inversion in the refinement calculus, Verification of knowledge bases based on containment checking, Domain semantics of possibility computations, Verifiable properties of database transactions, The Spatial Semantic Hierarchy, Simplification of boolean verification conditions, A space-efficient self-stabilizing algorithm for measuring the size of ring networks, Quantitative semantics, topology, and possibility measures, A weakest precondition semantics for communicating processes, On infinite computations in denotational semantics, Programs as proofs: A synopsis, Fair termination revisited - with delay, Ten years of Hoare's logic: A survey. II: Nondeterminism, Coordinating action systems, A linear-time algorithm for a special case of disjoint set union, Fairness and conspiracies, MLOG: A strongly typed confluent functional language with logical variables, Quantitative program logic and expected time bounds in probabilistic distributed algorithms., Nondeterminacy and recursion via stacks and games, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, The probe: An addition to communication primitives, Decentralized state feedback control of discrete event systems, Quasi-boolean equivalence, Weakest pre-condition reasoning for Java programs with JML annotations, A relational division operator: The conjugate kernel, A denotational semantics for low-level probabilistic programs with nondeterminism, Real algebraic numbers and polynomial systems of small degree, The laws of Occam programming, Three Debates about Computing, Linear logic automata, Programming from Galois connections, Conditioning in probabilistic programming, Combining relational calculus and the Dijkstra-Gries method for deriving relational programs, Data Refinement with Probability in Mind, Proof rules for the correctness of quantum programs, Evaluation strategies for functional logic programming, A predicate/state transformer semantics for Bayesian learning, Semantics of non-deterministic possibility computation, Observations in using parallel and sequential evolutionary algorithms for automatic software testing, Verification of concurrent programs: The automata-theoretic framework, Boolean restriction categories and taut monads, Partial correctness for probabilistic demonic programs, The correctness of nondeterministic programs revisited, A new generalization of Dekker's algorithm for mutual exclusion, The automated proof of a trace transformation for a bitonic sort, An inventory decision support system using the object oriented approach, A data structure for dynamic trees, On the notion of expressiveness and the rule of adaptation, Probabilistic analysis of algorithms for the Dutch national flag problem, Analyzing a \(\chi\) model of a turntable system using Spin, CADP and Uppaal, A theory for execution-time derivation in real-time programs, Probabilistic guarded commands mechanized in HOL, Hybrid action systems, Contracts, games, and refinement., Infinite executions of lazy and strict computations, A greedy algorithm for dropping digits, Annotation inference for modular checkers, Derivation of a rotator circuit with homogeneous interconnect, Optimal real-time garbage collection for acyclic pointer structures, Stepwise refinement of sequence diagrams with soft real-time constraints