Abstract Variants of Kleene algebra have been used to provide foundations of reasoning about programs, for instance by representing Hoare Logic (HL) in algebra. That work has generally emphasised program correctness, i.e., proving the absence of bugs. Recently, Incorrectness Logic (IL) has been advanced as a formalism for the dual problem: proving the presence of bugs. IL is intended to underpin the use of logic in program testing and static bug finding. Here, we use a Kleene algebra with diamond operators and countable joins of tests, which embeds IL, and which also is complete for reasoning about the image of the embedding. Next to embedding IL, the algebra is able to embed HL, and allows making connections between IL and HL specifications. In this sense, it unifies correctness and incorrectness reasoning in one formalism.

The talk extends the Laws of Programming [1] by four laws governing concurrent composition of programs. This operator is associative and commutative and distributive through union; and it has the same unit (do nothing) as sequential composition. Furthermore, sequential and concurrent composition distribute through each other, in accordance with an exchange law; this permits an implementation of concurrency by partial interleaving.

Share on Message of thanks: on the receipt of the 2011 ACM SIGPLAN distinguished achievement award Author: Tony Hoare Microsoft Research, Cambridge, United Kingdom Microsoft Research, Cambridge, United KingdomView Profile Authors Info & Claims POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 2012 Pages 3–6https://doi.org/10.1145/2103656.2103659Published:25 January 2012Publication History 1citation355DownloadsMetricsTotal Citations1Total Downloads355Last 12 Months5Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Abstract We survey the well-known algebraic laws of sequential programming, and extend them with some less familiar laws for concurrent programming. We give an algebraic definition of the Hoare triple, and algebraic proofs of all the relevant laws for concurrent separation logic. We give the provable concurrency laws for Milner transitions, for the Back/Morgan refinement calculus, and for Dijkstra’s weakest preconditions. We end with a section in praise of algebra, of which Carroll Morgan is such a master.

The ideal of verified software has long been the goal of research in Computer Science. This paper argues that the time is ripe to embark on a Grand Challenge project to construct a program verifier, based on a sound and complete theory of programming, and evaluated by experimental application to a representative sample of useful computer software.

The cultures of science and engineering are diametrically opposed along a number of dimensions: long-term/short-term, idealism/compromise, formality/ intuition, certainty/risk management, perfection/ adequacy, originality/familiarity, generality/specificity, unification/diversity, separation/amalgamation of concerns. You would expect two such radically different cultures to collide. Yet all the technological advances of the modern era result not from their collision but from their collusion-in its original sense of a fruitful interplay of ideas from both cultures. The author illustrates these points by the example of research into program verification and research into dependability of systems. The first of these aims at development and exploitation of a grand unified theory of programming, and therefore shares more the culture of science. The second is based on practical experience of projects in a range of important computer applications, and it shares more the culture of engineering. A collision of cultures would not be unexpected. But the author suggests that the time has come for collusion, and the author suggests how. We need to define an interface across which the cultures can explicitly collaborate. Dependability research can deliver its results in the form of a library of realistic domain models for a variety of important and common computer applications. A domain model is a reusable pattern for many subsequently conceived products or product lines. It includes a mix of informal and formal descriptions of the environment in which the computer system or network is embedded. It concentrates on the interfaces to the computer system, and the likely requirements and preferences of its community of users. The practicing software engineer takes the relevant application domain model as the starting point for a new project or project proposal, and then specializes it to accord with the current environment and current customer requirements. Domain models are most likely to emerge as the deliverable result of good research into dependability. If the available tools are powerful enough, verification can begin already at this stage to deliver benefit, by checking the consistency of formalized requirements, and detecting possible feature interactions. Ideally, implementation proceeds from then on in a manner that ensures correctness by construction. At all stages the project should be supported by verification tools. That is the long-term goal of a new initiative in verified software, which is under discussion by the international computing research community. This initiative has both a scientific strand and an engineering strand. The scientific strand develops the necessary unified and comprehensive theories of programming; it implements the tools that apply the theory to actual program verification; and it tests both the theory and the tools by application to a representative corpus of real or realistic programs. The engineering strand develops a library of domain models and specifications which enable practicing engineers to apply the theory and the tools to new programs in the relevant application domain. We hope that the results of this research will contribute to the reduction of the current significant costs of programming error. To achieve this will require a successful collusion of the scientific and engineering cultures.

The ideal of verified software has long been the goal of research in Computer Science. This article argues that the time is ripe to embark on a Grand Challenge project to construct a program verifier, based on a sound and complete theory of programming, and evaluated by experimental application to a large and representative sample of useful computer software. Computer Science owes its existence to the invention of the stored-program digital computer. It derives continuously renewed inspiration from the constant stream of new computer applications, which are still being opened up by half a century of continuous reduction in the cost of computer chips, and by spectacular increases in their reliability, performance and capacity. The science of programming has made comparable advances with the discovery of faster and more general algorithms, and with the development of a wide range of specific application programs, spreading previously unimaginable benefits into almost all aspects of human life.

We study a family of implementations for linked lists using fine-grain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical, coarse-grain synchronisation. Our examples are demonstrative of common design patterns such as lock coupling, optimistic, and lazy synchronisation. Although they are are highly concurrent, we prove that they are linearisable, safe, and they correctly implement a high-level abstraction. Our proofs illustrate the power and applicability of rely-guarantee reasoning, as well of some of its limitations. The examples of the paper establish a benchmark challenge for other reasoning techniques.

Abstract The verified software repository is dedicated to a long-term vision of a future in which all computer systems justify the trust that society increasingly places in them. This would be accompanied by a substantial reduction in the current high costs of programming error, incurred during the design, development, testing, installation, maintenance, evolution, and retirement of computer software. An important technical contribution to this vision will be a verifying compiler: a tool-set that automatically proves that a program will always meet its specification, insofar as this has been formalised, without even needing to run it. This has been a challenge for computing research for over 30 years, but the current state of the art now gives grounds for hope that it may be implemented in the foreseeable future. Achievement of the overall vision will depend also on continued progress of research into dependability and software evolution, as envisaged by the UKCRC Grand Challenge project in dependable systems evolution . The verified software repository is a first step towards the realisation of this long-term vision. It will maintain and develop an evolving collection of state-of-the-art tools, together with a representative portfolio of real programs and specifications on which to test, evaluate, and develop the tools. It will contribute initially to the inter-working of tools, and eventually to their integration. It will promote transfer of the relevant technology to industrial tools and into software engineering practice. It will build on the recognised achievements of practical formal development of safety-critical computer applications, and contribute to an international initiative in verified software, covering theory, tools, and experimental validation.

What are the major research challenges that face the world of computing today? Are there any of them that match the grandeur of well-known challenges in other branches of science? This article is a report on an exercise by the Computing Research Community in the UK to answer these questions, and includes a summary of the outcomes of a BCS-sponsored conference held in Newcastle-upon-Tyne from 29 to 31 March this year.

This contribution proposes a set of criteria that distinguish a grand challenge in science or engineering from the many other kinds of short-term or long-term research problems that engage the interest of scientists and engineers. As an example drawn from Computer Science, it revives an old challenge: the construction and application of a verifying compiler that guarantees correctness of a program before running it.

A theory of programming starts with a complete Boolean algebra of specifications, and defines healthiness conditions which exclude infeasibility of implementation. These are expressed as algebraic laws useful for transformation and optimisation of designs. Programming notations and languages must be restricted to those preserving all the healthiness conditions. We have explored a wide range of programming paradigms, including nondeterministic, sequential, parallel, logical and probabilistic. In all cases, we have found a single healthiness condition, formalised by constructions due to Karoubi and to Kleisli. The uniformity maintains for all paradigms a single notion of correctness throughout the chain that leads from specification through designs to programs that are proved to meet the original specification.

Some modern superscalar microprocessors provide only imprecise exceptions. That is, they do not guarantee to report the same exception that would be encountered by a straightforward sequential execution of the program. In exchange, they offer increased performance or decreased chip area (which amount to much the same thing).This performance/precision tradeoff has not so far been much explored at the programming language level. In this paper we propose a design for imprecise exceptions in the lazy functional programming language Haskell. We discuss several designs, and conclude that imprecision is essential if the language is still to enjoy its current rich algebra of transformations. We sketch a precise semantics for the language extended with exceptions.The paper shows how to extend Haskell with exceptions without crippling the language or its compilers. We do not yet have enough experience of using the new mechanism to know whether it strikes an appropriate balance between expressiveness and performance.

Journal Article Editorial Get access C.A.R HOARE C.A.R HOARE Oxford Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 4, Issue 3, June 1994, Pages 215–216, https://doi.org/10.1093/logcom/4.3.215 Published: 01 June 1994

Science makes progress by constructing mathematical models, deducing their observable consequences, and testing them by experiment. Successful theoretical models are later taken as the basis for engineering methods and codes of practice for design of reliable and useful products. Models can play a similar central role in the progress and practical application of Computing Science.A model of a computational paradigm starts with choice of a carrier set of potential direct or indirect observations that can be made of a computational process. A particular process is modelled as the subset of observations to which it can give rise. Process composition is modelled by relating observations of a composite process to those of its components. Indirect observations play an essential role in such compositions. Algebraic properties of the composition operators are derived with the aid of the simple theory of sets and relations. Feasibility is checked by a mapping from a more operational model.A model constructed as a family of sets is easily adapted as a calculus of design for total correctness. A specification is given by an arbitrary set containing all observations permitted in the required product. It should be expressed as clearly as possible with the aid of the full power of mathematics and logic. A product meets a specification if its potential observations form a subset of its permitted observations. This principle requires that all envisaged failure modes of a product are modelled as indirect observations, so that their avoidance can be proved. Specifications of components can be composed mathematically by the same operators as the components themselves. This permits top-down proof of correctness of designs even before their implementation begins. Algebraic properties and reasoning are helpful throughout development. Non-determinism is seen as no problem, but rather as a part of the solution.

Abstract The paper tells the story of the development over twenty‐five years of my ideas about communicating sequential processes. One of its most subtle and most useful facilities is the guarded choice, which appears as the ALT command in occam. Its subtleties are clarified and its usefulness increased by an understanding of the relevant simple algebraic laws, based on mathematical research conducted at Oxford. The abstractions provided by mathematics are the secret of the versatility of occam, which can be reliably and efficiently implemented by multiprogramming or by multiprocessing or by hardware, or by any combination of these. In conclusion, it is conjectured that the occam programming paradigm will remain the most efficient and most reliable for the general‐purpose shared‐store multiprocessors of the future.

Category theory offers a unified mathematical framework for the study of specifications and programs in a variety of styles, such as procedural, functional and concurrent. One way that these different languages may be treated uniformly is by generalising the definitions of some standard categorical concepts. In this paper we reproduce in the generalised theory analogues of some standard theorems on isomorphism, and outline their applications to programming languages.

The possibility of extending some of the logical methods that have been recommended for the design of software to the design of hardware, in particular, of synchronous switching circuits implemented in CMOS, is explored. The objective is to design networks that are known by construction. Things that can go wrong with circuits designed in this way are examined. The application of the techniques is discussed.>

A mathematical model for communicating sequential processes is given, and a number of its interesting and useful properties are stated and proved. The possibilities of nondetermimsm are fully taken into account.

This paper defines some "weakest precondltmn'" predicate transformers, Investigates their "healthiness" properties, and apphes them to Dljkstra's language of guarded commands It shows that Dljkstra's w~ function is not the weakest healthy one, but it ~s clearly the best one for practical programming, because it proves the absence of bhnd alleys from a nondetermmlsac program KEY WORDS AND PHRASES.formal language defimtlon, axmmatlc approach to programming, weakest precondmons, predicate transformers, healthiness condmons, nondetermlnacy, guarded commands, blind alleys, program traces, complementary language definitions CR CATEGORIES 4 20, 5 23, 5 24 General

Many descriptions of Fast Fourier Transform exist in the literature. Several of these appeal to matrix concepts, such as Kronecker multiplication. This paper shows the essential simplicity of the algorithm and the reasoning behind it. However it deals only with the case when the number of points is an exact power of 2.

Abstract Ambiguities and insecurities in the programming language Pascal are discussed.

Abstract This paper describes SIMONE, an extension of PASCAL,1 which provides the quasiparallel programming facility of SIMULA 67, but without classes or references. The language is intended to be suitable for the design, testing and simulation of operating system algorithms. It is illustrated by simple examples, suitable as project material in a course on operating systems. A simple, restricted, but efficient implementation is described. It is suggested that the language might be suitable for more general simulation purposes, and an example of a general job shop simulation is given.

The principles and practices of structured programming have been expounded and illustrated by relatively small examples (Dahl, Dijkstra, Hoare, 1972). Systematic methods for the construction of parallel algorithms have also been suggested (Dijkstra, 1968, a, b). This paper attempts to extend structured programming methods to a program intended to operate in a parallel environment, namely a paging system for the implementation of virtual store. The design decisions are motivated by considerations of cost of effectiveness. The purpose of a paging system is taken to be the sharing of main and backing store of a computer among a number of users making unpredictable demands upon them; and to do so in such a way that each user will not be concerned whether his information is stored at any given time on main or backing store. For the sake of definiteness, the backing store is taken here to be a sectored drum; but the system could readily be adapted for other devices. Our design does not rely on any particular paging hardware, and it should be implementable in any reasonable combination of hardware and software. Furthermore, it does not presuppose any particular structure of virtual store (linear, two-dimensional, ‘cactus’, etc.) provided to the user program.

This paper illustrates a method of constructing a program together with its proof. By structuring the program at two levels of abstraction, the proof of the more abstract algorithm may be completely separated from the proof of the concrete representation. In this way, the overall complexity of the proof is kept within more reasonable bounds.

This paper gives the proof of a useful and non-trivial program, Quicksort (Hoare, 1961). First the general algorithm is described informally; next a rigorous but informal proof of correctness of the coded program is given; finally some formal methods are introduced. Conclusions are drawn on the possibility of enlisting mechanical aid in the proof process.

ALGOL 60 Implementation B. Randell and L. J. Russell , 1964 ; 418. (London : Academic Press Inc. , 84s.)

A description of the method of specifying input and output in ALGOL programs run on the National-Elliott 803 and the Elliott 503 digital computers.

A description is given of a new method of sorting in the random-access store of a computer. The method compares very favourably with other known methods in speed, in economy of storage, and in ease of programming. Certain refinements of the method, which may be useful in the optimization of inner loops, are described in the second part of the paper.