Formal Methods (FMs) radically improve the quality of the code artefacts they help to produce. They are simple, probably accessible to first-year undergraduate students and certainly to second-year students and beyond. Nevertheless, in many cases, they are not part of a general recommendation for course curricula, i.e., they are not taught — and yet they are valuable. One reason for this is that teaching “Formal Methods” is often confused with teaching logic and theory. This article advocates what we call FM thinking : the application of ideas from Formal Methods applied in informal, lightweight, practical and accessible ways. We will argue here that FM thinking should be part of the recommended curriculum for every Computer Science student, for even students who train only in that “thinking” will become much better programmers. However, there will be others who, exposed to those ideas, will be ideally positioned to go further into the more theoretical background: why the techniques work, how they can be automated, and how new ones can be developed. Those students would follow subsequently a specialised, more theoretical stream, including topics such as semantics, logics, verification and proof-automation techniques.

Abstract This paper draws together four perspectives that contribute to a new understanding of probability and solving problems involving probability. The first is the Subjective Bayesian perspective that probability is affected by one’s knowledge, and that it is updated as one’s knowledge changes. The main criticism of the Bayesian perspective is the problem of assigning prior probabilities; this problem disappears with our Information Theory perspective, in which we take the bold new step of equating probability with information. The main point of the paper is that the formal perspective (formalize, calculate, unformalize) is beneficial to solving probability problems. And finally, the programmer’s perspective provides us with a suitable formalism. To illustrate the benefits of these perspectives, we completely solve the hitherto open problem of the two envelopes.

This roadmap describes ways that researchers in four areas---specification languages, program generation, correctness by construction, and programming languages---might help further the goal of verified software. It also describes what advances the "verified software" grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas.A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.

Abstract. Time and space limitations can be specified, and proven, in exactly the same way as functionality. Proofs of time bounds, both implementation-independent and real-time, and of space requirements, both worst-case and average-case, are given in complete detail.

A. Joe Turner

Our premise is that programming languages should be designed to facilitate a programming methodology. We begin with the methodology of Michael Jackson; the notation that results is similar to Hoare's communicating sequential processes. Data and processing structures are described together in one grammatical formalism.

In the above paper,1Baber describes a scheme for representing data items with unlimited length. We would like to argue that this scheme is not very different from other published schemes and that his scheme is not obviously useful for the proposed application.

Previous article Full AccessCorrigendum. A New Representation of the Rational Numbers for Fast Easy ArithmeticE. C. R. Hehner and R. N. S. HorspoolE. C. R. Hehner and R. N. S. Horspoolhttps://doi.org/10.1137/0209019PDFBibTexSections ToolsAdd to favoritesExport CitationTrack CitationsEmail SectionsAbout"Corrigendum. A New Representation of the Rational Numbers for Fast Easy Arithmetic." SIAM Journal on Computing, 9(1), p. 217 Previous article FiguresRelatedReferencesCited ByDetails Volume 9, Issue 1| 1980SIAM Journal on Computing History Submitted:12 July 1979Published online:13 July 2006 InformationCopyright © 1980 Society for Industrial and Applied MathematicsPDF Download Article & Publication DataArticle DOI:10.1137/0209019Article page range:pp. 217-217ISSN (print):0097-5397ISSN (online):1095-7111Publisher:Society for Industrial and Applied Mathematics

A novel system for representing the rational numbers based on Hensel’s p-adic arithmetic is proposed. The new scheme uses a compact variable-length encoding that may be viewed as a generalization of radix complement notation. It allows exact arithmetic, and approximate arithmetic under programmer control. It is superior to existing coding methods because the arithmetic operations take particularly simple, consistent forms. These attributes make the new number representation attractive for use in computer hardware.

The p-adic number system is introduced and developed into a form suitable for performing exact arithmetic in computers. The proposed representation has several desirable attributes: the four standard arithmetic operations have a simple consistent form, the programmer has the ability to choose the precise degree of accuracy in his calculations and the variable-length nature of the representation achieves compact encodings.

Structuring can be defined independently of what is being structured, and can be applied profitably to more than one domain. Using one mechanism to structure both values and assignments, we obtain equivalents for a variety of data and control structures. Structuring assignments is preferable to structuring control: the former is more conducive to a mathematical style of programming while the latter is more conducive to tracing.

The problem of determining the minimum representation of programs for execution by a computer is considered. The methods of measuring space requirements suggest practical methods for encoding programs and for designing machine languages. An analysis of the operation portion of instructions finds that the 47 operation codes used by a well-known compiler require, on average, fewer than two bits each.