Formal derivation of rule-based programs

It is shown that a combination of specification and program refinement may be applied to deriving efficient concurrent rule-based programs. Specification refinement is used to generate an initial rule-based program that is refined into a program which is highly concurrent and efficient. This program derivation strategy is divided into two major tasks. The first task relies on specification refinement. Techniques similar to those employed in the derivation of UNITY programs are used to produce a correct rule-based program having a static knowledge base. The second task involves program refinement and is specific to the development of concurrent rule-based programs. It relies heavily on the availability of a computational model, such as Swarm, that has the ability to dynamically restructure the knowledge base. The ways in which a Swarm program can be translated to OPS5 specifically, given some restrictions, while maintaining the correctness criteria are discussed     

A decompositional approach to the design of parallel programs

A methodology for the derivation of parallel implementations from program specifications is developed. The goal of the methodology is to decompose a program specification into a collection of module specifications via property refinement, such that each module may be implemented independently by a subprogram. The correctness of the implementation is then deduced from the correctness of the property refinement procedure and the correctness of the individual subprograms. The refinement strategy is based on identifying frequently occurring control structures such as sequential composition and iteration. The methodology is developed in the context of the UNITY logic and the UC programming language, and illustrated through the solution of diffusion aggregation in fluid flow simulations     

Using refinement calculus techniques to prove linearizability

Stepwise refinement is a method for systematically transforming a high-level program into an efficiently executable one. A sequence of successively refined programs can also serve as a correctness proof, which makes different mechanisms in the program explicit. We present rules for refinement of multi-threaded shared-variable concurrent programs. We apply our rules to the problem of verifying linearizability of concurrent objects, that are accessed by an unbounded number of concurrent threads. Linearizability is an established correctness criterion for concurrent objects, which states that the effect of each method execution can be considered to occur atomically at some point in time between its invocation and response. We show how linearizability can be expressed in terms of our refinement relation, and present rules for establishing this refinement relation between programs by a sequence of local transformations of method bodies. Contributions include strengthenings of previous techniques for atomicity refinement, as well as an absorption rule, which is particularly suitable for reasoning about concurrent algorithms that implement atomic operations. We illustrate the application of the refinement rules by proving linearizability of Treiber’s concurrent stack algorithm and Michael and Scott’s concurrent queue algorithm.     

一种基于程序正确性证明理论的程序开发方法

程序的形式推导方法是一种基于程序正确性证明理论的程序开发方法,它使得程序的开发和证明同时进行,程序开发完成的同时其正确性亦得以保 证,以两个问题的程序开发为例说明了程序的形式推导方法的使用。     

Provably correct derivation of algorithms using FermaT

The transformational programming method of algorithm derivation starts with a formal specification of the result to be achieved, plus some informal ideas as to what techniques will be used in the implementation. The formal specification is then transformed into an implementation, by means of correctness-preserving refinement and transformation steps, guided by the informal ideas. The transformation process will typically include the following stages: (1) Formal specification (2) Elaboration of the specification, (3) Divide and conquer to handle the general case (4) Recursion introduction, (5) Recursion removal, if an iterative solution is desired, (6) Optimisation, if required. At any stage in the process, sub-specifications can be extracted and transformed separately. The main difference between this approach and the invariant based programming approach (and similar stepwise refinement methods) is that loops can be introduced and manipulated while maintaining program correctness and with no need to derive loop invariants. Another difference is that at every stage in the process we are working with a correct program: there is never any need for a separate “verification” step. These factors help to ensure that the method is capable of scaling up to the development of large and complex software systems. The method is applied to the derivation of a complex linked list algorithm and produces code which is over twice as fast as the code written by Donald Knuth to solve the same problem.     

Contracts,Games, and Refinement

We consider the notion of a contract that governs the behavior of a collection of agents. In particular, we study the question of whether a group among these agents can achieve a given goal by following the contract. We show that this can be reduced to studying the existence of winning strategies in a two-person game. A notion of correctness and refinement is introduced for contracts and contracts are shown to form a lattice and a monoid with respect to the refinement ordering. We define a weakest precondition semantics for contracts that permits us to compute the initial states from which a group of agents has a winning strategy to reach their goal. This semantics generalizes the traditional predicate transformer semantics for program statements to contracts and games. Ordinary programs and interactive programs are special kinds of contracts.     

一种基于构件演算的主动构件精化方法

现代构件系统通常包含多个并发执行的主动构件,这使得验证构件系统的正确性变得十分困难.通过对构件演算进行扩展,提出了一种主动构件的精化方法.在构件接口层引入契约.契约使用卫式设计描述公共方法和主动活动的功能规约.通过一对发散、失败集合定义契约的动态行为,并利用发散、失败集合之间的包含关系定义契约间的精化关系.证明了应用仿真技术确认契约精化关系的定理.定义构件的语义为其需求接口契约到其服务接口契约的函数,以此为基础,可以通过契约的精化来证明构件的精化.给出了构件的组装规则.在构件系统自底向上的构造过程中,应用构件的精化方法和组装规则可以保证最终系统的正确性.     

Relation-algebraic semantics

The first half is a tutorial on orderings, lattices, Boolean algebras, operators on Boolean algebras, Tarski's fixed point theorem, and relation algebras.

In the second half, elements of a complete relation algebra are used as “meanings” for program statements. The use of relation algebras for this purpose was pioneered by de Bakker and de Roever in [10–12]. For a class of programming languages with program schemes, single μ-recursion, while-statements, if-then-else, sequential composition, and nondeterministic choice, a definition of “correct interpretation” is given which properly reflects the intuitive (or operational) meanings of the program constructs. A correct interpretation includes for each program statement an element serving as “input/output relation” and a domain element specifying that statement's “domain of nontermination”. The derivative of Hitchcock and Park [17] is defined and a relation-algebraic version of the extension by de Bakker [8, 9] of the Hitchcock-Park theorem is proved. The predicate transformers wp_s(-) and wlp_s(-) are defined and shown to obey all the standard laws in [15]. The “law of the excluded miracle” is shown to hold for an entire language if it holds for that language's basic statements (assignment statements and so on). Determinism is defined and characterized for all the program constructs. A relation-algebraic version of the invariance theorem for while-statements is given. An alternative definition of intepretation, called “demonic”, is obtained by using “demonic union” in place of ordinary union, and “demonic composition” in place of ordinary relational composition. Such interpretations are shown to arise naturally from a special class of correct interpretations, and to obey the laws of wp_s(-).     

Verification conditions are code

This paper presents a new theoretical result concerning Hoare Logic. It is shown here that the verification conditions that support a Hoare Logic program derivation are themselves sufficient to construct a correct implementation of the given pre-, and post-condition specification. This property is mainly of theoretical interest, though it is possible that it may have some practical use, for example if predicative programming methodology is adopted. The result is shown to hold for both the original, partial correctness, Hoare logic, and also a variant for total correctness derivations.     

Encoding, Decoding and Data Refinement

Data refinement is the systematic replacement of a data structure with another one in program development. Data refinement between program statements can on an abstract level be described as a commutativity property where the abstraction relationship between the data structures involved is represented by an abstract statement (a decoding). We generalise the traditional notion of data refinement by defining an encoding operator that describes the least (most abstract) data refinement with respect to a given abstraction. We investigate the categorical and algebraic properties of encoding and describe a number of special cases, which include traditional notions of data refinement. The dual operator of encoding is decoding, which we investigate and give an intuitive interpretation to. Finally we show a number of applications of encoding and decoding. Received May 1999 / Accepted in revised form November 2000     

SPARE: a development environment for program analysis algorithms

A tool that bridges the gap between the theory and practice of program analysis specifications is described. The tool supports a high-level specification language that enables clear and concise expression of analysis algorithms. The denotational nature of the specifications eases the derivation of formal proofs of correctness for the analysis algorithm. SPARE (structured program analysis refinement environment) is based on a hybrid approach that combines the positive aspects of both the operational and the semantics-driven approach. An extended denotational framework is used to provide specifications in a modular fashion. Several extensions to the traditional denotational specification language have been designed to allow analysis algorithms to be expressed in a clear and concise fashion. This extended framework eases the design of analysis algorithms as well as the derivation of correctness proofs. The tool provides automatic implementation for testing purposes     

Program development by inductive stepwise refinement

A constructive method of program development is presented. It seeks to unify two important ideas about program development. Namely that programming is a goal-oriented activity and that there should be a correspondence between data and program structures. The latter concept is seen to be extensible beyond the data processing context in which it was originally proposed. Induction provides the vehicle for program development by stepwise refinement, with the final program being constructed by application of a sequence of progressively more powerful generalizations. The design process employed guarantees the correctness of the final program provided that each of the refinement steps have been correctly taken. The method is illustrated by a number of samples.     

Measurement of refinement and correctness

The purpose of this paper is to introduce a measurement approach of refinement and correctness of probabilistic programs. That is, we define the refinement degree and the correctness degree by the weakest precondition transformers. This kind of measurement indicates the degree that a program is refined by another and the degree that a program is correct with respect to a pair of precondition and postcondition. Some properties of this measurement, for example continuity, are discussed.     

Program and proof optimizations with type systems

We demonstrate a method for describing data-flow analyses based program optimizations as compositional type systems with a transformation component. Analysis results are presented in terms of types ascribed to expressions and statements, certifiable by type derivations, and the transformation component carries out the optimizations that the type derivations license. We describe dead code elimination and common subexpression elimination. In the case of common subexpression elimination we circumvent non-compositionality with a combined type system for a combination of two analyses. The motivation of this work lies in certified code applications, where an optimization of a program must be supported by a checkable justification. As an example application we highlight “proof optimization”, i.e., mechanical transformation of a program’s functional correctness proof together with the program, based on the analysis type derivation.     

Refinement concepts formalised in higher order logic

A theory of commands with weakest precondition semantics is formalised using the HOL proof assistant system. The concept of refinement between commands is formalised, a number of refinement rules are proved and it is shown how the formalisation can be used for proving refinements of actual program texts correct.     

An algebraic treatment of procedure refinement to support mechanical verification

We introduce a new algebraic model for program variables, suitable for reasoning about recursive procedures with parameters and local variables in a mechanical verification setting. We give a predicate transformer semantics to recursive procedures and prove refinement rules for introducing recursive procedure calls, procedure parameters, and local variables. We also prove, based on the refinement rules, Hoare total correctness rules for recursive procedures, and parameters. We introduce a special form of Hoare specification statement which alone is enough to fully specify a procedure. Moreover, we prove that this Hoare specification statement is equivalent to a refinement specification. We implemented this theory in the PVS theorem prover.This work is based on an earlier work: Reasoning about recursive procedures with parameters. In Proceedings of the Workshop on Mechanized Reasoning about Languages with Variable Binding, 2003, Uppsala, Sweden, ACM Press.Received March 2004Revised October 2004Accepted February 2005 by C. B. Jones     

Granularity-Driven Dynamic Predicate Slicing Algorithms for Message Passing Systems

Program Slicing is a well-known decomposition technique that transforms a large program into a smaller one that contains only statements relevant to the computation of a selected function. In this paper, we present two novel predicate-based dynamic slicing algorithms for message passing programs. Unlike more traditional slicing criteria that focus only on parts of the program that influence a variable of interest at a specific position in the program, a predicate focuses on those parts of the program that influence the predicate. The dynamic predicate slices capture some global requirements or suspected error properties of a distributed program and computes all statements that are relevant. The presented algorithms differ from each other in their computational approaches (forward versus backward) and in the granularity of information they provide. A proof of correctness of these algorithms is provided. Through the introduction of dominant states and dominant events, critical statement executions are identified that change the value of the global predicate. Under this formulation, optimizing dynamic predicate slicing becomes a meaningful goal as well. Finally, we present how predicate slices can be applied to support comprehension tasks for analyzing and maintaining distributed programs.     

扩展时段时序逻辑的模型、一致性和推理

给出了扩展时段时序逻辑的时间Petri网（TPN）模型构造方法，在构造模型的同时对时序关系进行一致性检验，在模型的基础上提出了一种时序关系推理算法，这种推理算法基于TPN模型的性质及基本不等式规则，可由一组已知的扩展时段时序关系推出一些未知的扩展时段时序关系，这种推广理算法的优势在于利用了TNP模型的分析技术，减小了推理的时间复杂度比单纯利用不等式规则的推理更直观，也更简单，是一种有效的方法，最后，对扩展时段时序逻辑的TPN模型进行了扩充，增强了其模型和分析的能力。     

PELAS-program error-locating assistant system

Error localization in program debugging is the process of identifying program statements which cause incorrect behavior. A prototype of the error localization assistant system which guides a programmer during debugging of Pascal programs is described. The system is interactive: it queries the programmer for the correctness of the program behavior and uses answers to focus the programmer's attention on an erroneous part of the program (in particular, it can localize a faulty statement). The system differs from previous approaches in that it makes use of the knowledge of program structure, which is derived automatically. The knowledge of program structure is represented by the dependence network which is used by the error-locating reasoning mechanism to guide the construction, evaluation, and modification of hypothesis of possible causes of the error. Backtracking reasoning has been implemented in the reasoning mechanism