Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

We present a fully abstract weakest precondition calculus and its integration with symbolic execution. Our assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from a specific implementation of object creation. Objects which are not (yet) created never play any role. The corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and proof rules is illustrated with an example of a linked list reachability property. All proof rules presented are fully implemented in a version of the KeY verification system for Java programs.     

A proof outline logic for object-oriented programming

This paper describes a proof outline logic that covers most typical object-oriented language constructs in the presence of inheritance and subtyping. The logic is based on a weakest precondition calculus for assignments and object allocation which takes field shadowing into account. Dynamically bound method calls are tackled with a variant of Hoare's rule of adaptation that deals with the dynamic allocation of objects in object-oriented programs. The logic is based on an assertion language that is closely tailored to the abstraction level of the programming language.     

Observable behavior of distributed systems: Component reasoning for concurrent objects

Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. Rather than performing analysis at the level of code in, e.g., Java or C++, we consider the analysis of such systems at the level of an abstract, executable modeling language. This language, based on concurrent objects communicating by asynchronous method calls, avoids some difficulties of mainstream object-oriented programming languages related to compositionality and aliasing. To facilitate system analysis, compositional verification systems are needed, which allow components to be analyzed independently of their environment. In this paper, a proof system for partial correctness reasoning is established based on communication histories and class invariants. A particular feature of our approach is that the alphabets of different objects are completely disjoint. Compared to related work, this allows the formulation of a much simpler Hoare-style proof system and reduces reasoning complexity by significantly simplifying formulas in terms of the number of needed quantifiers. The soundness and relative completeness of this proof system are shown using a transformational approach from a sequential language with a non-deterministic assignment operator.     

An abstract programming language and correctness proofs

The realization of an abstract programming language is a good approach for automating the software production process and facilitating the correctness proof of a software system.

This paper introduces a formal language for programming at the abstract level by combining Pascal with VDM (Vienna Development Method). The notation provided by the language obliges programmers to consider the correctness of programs throughout the whole process of programming, and the proof axiom and rules presented in this paper may be used to prove the correctness of programs. A complete example is given to illustrate how to program using APL and how to prove the correctness of programs using the given axiom and rules.     

Backwards type analysis of asynchronous method calls

Asynchronous method calls have been proposed to better integrate object orientation with distribution. In the language, asynchronous method calls are combined with so-called processor release points in order to allow concurrent objects to adapt local scheduling to network delays in a very flexible way. However, asynchronous method calls complicate the type analysis by decoupling input and output information for method calls, which can be tracked by a type and effect system. Interestingly, backwards type analysis simplifies the effect system considerably and allows analysis in a single pass. This paper presents a kernel language with asynchronous method calls and processor release points, a novel mechanism for local memory deallocation related to asynchronous method calls, an operational semantics in rewriting logic for the language, and a type and effect system for backwards analysis. Source code is translated into runtime code as an effect of the type analysis, automatically inserting inferred type information in method invocations and operations for local memory deallocation in the process. We establish a subject reduction property, showing in particular that method lookup errors do not occur at runtime and that the inserted deallocation operations are safe.     

Correctness of programs with Pascal-like procedures without global variables

We study a programming language L_Pas consisting of blockstructured programs with a Pascal-like procedure concept which allows procedures as parameters. Due to Clarke (1979) there cannot be any sound and relatively complete Hoare-like system proving partial correctness for the full language L_Pas. However, in Langmaack and Olderog (1980) it has been conjectured that such a system exists once global variables are disallowed.In this paper we prove a slightly weaker version of this conjecture by presenting a Hoare-like system which is sound and g-complete for all programs in L_Pas without global variables; g-completeness means completeness modulo a special second-order theory and an appropriate notion of expressiveness. The proof system provides new methods of dealing with procedures which are formalized in the Rule of Separation for procedure calls. The completeness proof for the system is carried out in a transparent way using modified formal computation trees. An example shows how to apply the proposed methods.     

An Asynchronous Communication Model for Distributed Concurrent Objects

Distributed systems are often modeled by objects that run concurrently, each with its own processor, and communicate by synchronous remote method calls. This may be satisfactory for tightly coupled systems, but in the distributed setting synchronous external calls lead to much waiting; at best resulting in inefficient use of processor capacity, at worst resulting in deadlock. Furthermore, it is difficult to combine active and passive behavior in concurrent objects. This paper proposes an object-oriented solution to these problems by means of asynchronous method calls and conditional processor release points. Although at the cost of additional internal nondeterminism in the objects, this approach seems attractive in asynchronous or unreliable environments. The concepts are integrated in a small object-oriented language with an operational semantics defined in rewriting logic, and illustrated by examples. This paper extends and combines results which have appeared in the proceedings of the 2004 International Conference on Software Engineering and Formal Methods (SEFM) [37] and the 2004 International Workshop on Rewriting Logic and its Applications (WRLA) [41].     

Proofs of randomized algorithms in Coq

Randomized algorithms are widely used for finding efficiently approximated solutions to complex problems, for instance primality testing and for obtaining good average behavior. Proving properties of such algorithms requires subtle reasoning both on algorithmic and probabilistic aspects of programs. Thus, providing tools for the mechanization of reasoning is an important issue. This paper presents a new method for proving properties of randomized algorithms in a proof assistant based on higher-order logic. It is based on the monadic interpretation of randomized programs as probabilistic distributions (Giry, Ramsey and Pfeffer). It does not require the definition of an operational semantics for the language nor the development of a complex formalization of measure theory. Instead it uses functional and algebraic properties of unit interval. Using this model, we show the validity of general rules for estimating the probability for a randomized algorithm to satisfy specified properties. This approach addresses only discrete distributions and gives rules for analyzing general recursive functions.We apply this theory to the formal proof of a program implementing a Bernoulli distribution from a coin flip and to the (partial) termination of several programs. All the theories and results presented in this paper have been fully formalized and proved in the Coq proof assistant.     

Knowledge object modeling

Knowledge objects are an integration of the object-oriented paradigm with logic rules. The proper integration provides a flexible and powerful environment, as rule-based components provide facilities for deductive retrieval and pattern matching, and object-oriented components provide a clear intuitive structure for programs in the form of class hierarchies. Based on the knowledge object concept, this paper presents a factor-centered representation language, Factor++, which models logic rules into the object-oriented paradigm, and a scheduling system, Schedular, using the Factor++ framework The construction of Schedular demonstrates that by using an object-oriented representation of knowledge objects, users can be given explicit control of the object hierarchy to customize the system to their particular needs, which includes letting users select among scheduling and other methods. In Schedular, rules are designed as derivation rules and constraint rules. The purpose of rules is either to restrict object structure and behavior, or to infer new data from the existing data. Rules are arranged in positions so that object methods are automatically firing up if environment changes are detected by these rules     

Towards a transformational approach to program verification

Although most typically used in other contexts, program transformations can simplify program verification by transforming a program containing complex language features into a semantically equivalent program containing only simpler language features. The proof of the transformed program can then be performed using a set of proof rules for only the simpler features. There are tradeoffs between the transformational approach and the standard approach to program verification with regard to proof understandability and compactness of programs and assertions, establishing soundness of the program verification method, and providing mechanized support for the method. The transformational approach has clear advantages in some of these aspects. This paper illustrates this transformational approach by considering proof rules for escape statements in iterative constructs, and discusses the tradeoffs with respect to its use. It also suggests how the approach can be applied to other language constructs, including some involving concurrency, and to solving some problems connected with the development of Hoare axiomatizations. Copyright © 1999 John Wiley & Sons, Ltd.     

Verification of object-oriented programs: A transformational approach

We show that verification of object-oriented programs by means of the assertional method can be achieved in a simple way by exploiting a syntax-directed transformation from object-oriented programs to recursive programs. This transformation suggests natural proofs rules and its correctness helps us to establish soundness and relative completeness of the proposed proof system. One of the difficulties is how to properly deal in the assertion language with the instance variables and aliasing. The discussed programming language supports arrays, instance variables, failures and recursive methods with parameters. We also explain how the transformational approach can be extended to deal with other features of object-oriented programming, like classes, inheritance, subtyping and dynamic binding.     

Mechanically verifying concurrent programs with the Boyer-Mooreprover

A proof system suitable for the mechanical verification of concurrent programs is described. This proof system is based on Unity, and may be used to specify and verify both safety and liveness properties. However, it is defined with respect to an operational semantics of the transition system model of concurrency. Proof rules are simply theorems of this operational semantics. This methodology makes a clear distinction between the theorems in the proof system and the logical inference rules and syntax which define the underlying logic. Since this proof system essentially encodes Unity in another sound logic, and this encoding has been mechanically verified, this encoding proves the soundness of this formalization of Unity. This proof system has been mechanically verified by the Boyer-Moore prover. This proof system has been used to mechanically verify the correctness of a distributed algorithm that computes the minimum node value in a tree     

A Structured Temporal Logic Language:XYZ/SE

In order to enhance the readability and to simplify the verification of temporal logic programs in the XYZ system,we propose a structured temporal logic language called XYZ/SE,based on XYZ/BE which is the basis language of the XYZ system.A set of proof rules are given and proved to be sound and adequate for proving the partial correctness of XYZ/SE programs in a compositional way.Moreover,we show that every XYZ/BE program can be transformed into an equivalent XYZ/SE program.So we have developed a general conpositional verification method in the XYZ system concerning the sequential case.     

基于XML-RPC企业分布式数据处理

XML—RPC是基于XML，HTTP，可跨平台，并允许复杂的数据结构传递、处理、返回的RPC。针对目前企业中流行采用的集中式数据处理系统存在的问题，提出了采用基本XML—RPC实现分布式数据处理系统，目的在于让企业信息系统简单、高效、易扩充，并保证系统的动态平衡和容错性。     

Program proving: Coroutines

Summary Proof methods adequate for a wide range of computer programs have been given in [1–6]. This paper develops a method suitable for programs which incorporate coroutines. The implementation of coroutines described follows closely that given in SIMULA [7, 8], a language in which such features may be used to great advantage. Proof rules for establishing the correctness of coroutines are given and the method is illustrated by the proof of a useful program for histogram compilation.     

A delegation-based approach for the unanticipated dynamic evolution of distributed objects

Large information systems are typically distributed and cater to several client programs, with different needs. Traditional approaches to software development and deployment cannot handle situations where (i) the needs of one client application evolve over time, diverging from the needs of others, and (ii) when the server application cannot be shutdown for maintenance. In this paper, we propose an experimental framework for the unanticipated dynamic evolution of distributed objects that enables us to: (i) extend the behavior of distributed objects during run-time, requiring no shutdown, and (ii) offer different functionalities to different applications simultaneously. In our approach, new client programs can invoke behavioral extensions to server objects that are visible only to them, while legacy applications may continue to use the non-extended versions of the server. Our approach has the advantage of: (i) requiring no changes to the host programming language or to the virtual machine, and (ii) providing a transparent programming model to the developer. In this paper, we describe the problem of unanticipated dynamic evolution of distributed objects, the principles underlying our approach, and our prototype implementations for Java and C#. We conclude by discussing related work, and the extent to which our approach can be used to support industrial strength unanticipated evolution.     

LVT: a layered verification technique for distributed computing systems

This paper presents a layered verification technique, called LVT, for the verification of distributed computing systems with multiple component layers. Each lower layer in such a system provides services in support of functionality of the higher layer. By taking a very general view of programming languages as interfaces of systems, LVT treats each layer in a distributed computing system as a distributed programming language. Each relatively higher‐level language in the computing system is implemented in terms of a lower‐level language. The verification of each layer in a distributed computing system can then be viewed as the verification of implementation correctness for a distributed language. This paper also presents the application of LVT to the verification of a distributed computing system, which has three layers: a small high‐level distributed programming language; a multiple processor architecture consisting of an instruction set and system calls for inter‐process message passing; and a network interface. Programs in the high‐level language are implemented by a compiler mapping from the language layer to the multiprocessor layer. System calls are implemented by network services. LVT and its application demonstrate that the correct execution of a distributed program, most notably its inter‐process communication, is verifiable through layers. The verified layers guarantee the correctness of (1) the compiled code that makes reference to operating system calls, (2) the operating system calls in terms of network calls, and (3) the network calls in terms of network transmission steps. The specification and verification involved are carried out by using the Cambridge Higher Order Logic (HOL) theorem proving system. Copyright © 1999 John Wiley & Sons, Ltd.     

Verification and synthesis of addition programs under the rules of correctness of statements

Deductive verification and synthesis of binary addition programs are carried out on the base of the rules of proving the correctness for statements of the predicate programming language P. The paper presents key fragments of verification and synthesis of the programs for the Ripple carry, Carry look-ahead and Ling adders. The correctness conditions of the programs were translated into the specification language of the PVS verification system. The proof is found to be a tedious procedure as compared with the ordinary programming. However, for program synthesis, the development of theories and proofs on PVS are easier and faster than for program verification.     

Sound refactorings

Refactoring consists in restructuring an object-oriented program without changing its behaviour. In this paper, we present refactorings as transformation rules for programs written in a refinement language inspired on Java that allows reasoning about object-oriented programs and specifications. A set of programming laws is available for the imperative constructs of this language as well as for its object-oriented features; soundness of the laws is proved against a weakest precondition semantics. The proof that the refactoring rules preserve behaviour (semantics) is accomplished by the application of these programming laws and data simulation. As illustration of our approach to refactoring, we use our rules to restructure a program to be in accordance with a design pattern.     

An approach to automatic deductive synthesis of functional programs

The work deals with automatic deductive synthesis of functional programs. Formal specification of a program is taken as a mathematical existence theorem and while proving it, we derive a program and simultaneously prove that this program corresponds to given specification. Several problems have to be resolved for automatic synthesis: the choice of synthesis rules that allows us to derive the basic constructions of a functional program, order of rule application and choice of a particular induction rule. The method proposed here is based on the deductive tableau method. The basic method gives rules for functional program construction. To determine the proof strategy we use some external heuristics, including rippling. And for the induction hypothesis formation the combination of rippling and the deductive tableau method became very useful. The proposed techniques are implemented in the system ALISA (Automatic Lisp Synthesizer) and used for automatic synthesis of several functions in the Lisp language. The work has been partially supported by RFBR grant 05-01-00948a.