We start with a mathematical definition of a real interval as a closed, connected set of reals. Interval arithmetic operations (addition, subtraction, multiplication, and division) are likewise defined mathematically and we provide algorithms for computing these operations assuming exact real arithmetic. Next, we define interval arithmetic operations on intervals with IEEE 754 floating point endpoints to be sound and optimal approximations of the real interval operations and we show that the IEEE standard's specification of operations involving the signed infinities, signed zeros, and the exact/inexact flag are such as to make a correct and optimal implementation more efficient. From the resulting theorems, we derive data that are sufficiently detailed to convert directly to a program for efficiently implementing the interval operations. Finally, we extend these results to the case of general intervals, which are defined as connected sets of reals that are not necessarily closed.

Rhetoric versus modernism in computing Get access M. van EMDEN M. van EMDEN University of VictoriaCanada Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 2, Issue 5, October 1992, Pages 551–555, https://doi.org/10.1093/logcom/2.5.551 Published: 01 October 1992

Abstract Cleanroom programming and code inspections independently provide evidence that it is more efficient to postpone the testing of code to a later stage than is usually done. This paper argues that an additional gain in quality and efficiency of development can be obtained by structuring inspections by means of an inspection protocol. The written part of such a protocol is prepared by the programmer before the inspection. It is modelled on Floyd's method for the verification of flowcharts. However, the protocol differs from Floyd's method in being applicable in practice. Structured inspections gain this advantage by not attempting to be a proof; they are no more than an articulation of existing forms of inspection. With the usual method of structured programming it may be difficult to prepare the inspection protol. On the other hand, ‘assertion‐driven programming’ (of which an example is included in this paper) not only facilitates protocol preparation, but also the coding itself.

Horn clauses of first-order predicate logic can be regarded as a high-level programming language when SLD-resoluUon, a special-purpose resolution theorem prover, is used as interpreter.Consequently, the semantics of Horn clauses can be studied both by model-theoreuc and fixpomt methods (in the sense of Scott).This posslbihty is exploited here by identifying the least (greatest) fixpomt with a least (greatest) model Successful termination of SLD-resolution is characterized by least fixpomts A semantic characterization of t'mlte failure of SLD-resoluuon is given, which coincides with the greatest fixpomt only for a special case of clauses.It is shown that nondetermmistlc flowchart schemata of bounded nondeterminaey are modeled by this special case; the connection between finite fadure and greatest fixpomt is then used to give a semantic characterization of termmauon, blocking, and nontermination of such flowchart schemata Categories and Subject Descriptors" F 3 1 ILogics and Meanings of Programs]' Speofymg and Verifying and Reasoning about Programs--logics of programs, F 4.1 [Mathematlcal Logic and Formal Languagesl Mathematical Logic--logic programming, 1 2 3 [Artificial Intelligencel.Deduction and Theorem Proving-logic programming

A common basis is presented, for Floyd's method of inductive assertions and for the subgoal induction method of Morris and Wegbreit. This basis is provided by consequence verification, a method for verifying logic programs. We connect flowcharts with logic programs by giving a recursive definition of the set of all computations of a flowchart. This definition can be given in two ways: the recursion can run forward or backward. Both definitions can be expressed in logic, resulting in a logic program which is then subjected to consequence verification. Verification of the forward logic program is shown to be essentially Floyd's method; verification of the backward program corresponds similarly to subgoal induction.

This paper contains an exposition of the method of programming with verification conditions. Although this method has much in common with the one discussed by Dijkstra in A Disciplne of Programming, it is shown to have the advantage in simplicity and flexibility. The simplicity is the result of the method's being directly based on Floyd's inductive assertions The method is flexible becasue of the way in which the program is constructed in two stages. In the first stage, a set of verification conditions is collected which corresponds to a program in "flowgraph" form. In this stage sequencing control is of no concern to the progmmer. Control is introduced in the second stage, which consists of automatable applications of translation and optimization rules, resulting in conventional code. Although our method has no use for the sequencing primitives of "structured programming," it is highly secure and systematic.

Sentences in first-order predicate logic can be usefully interpreted as programs. In this paper the operational and fixpoint semantics of predicate logic programs are defined, and the connections with the proof theory and model theory of logic are investigated. It is concluded that operational semantics is a part of proof theory and that fixpoint semantics is a special case of model-theoretic semantics.