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 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.     

Derivation of a parsing algorithm in martin-löf's theory of types

Type Theory is a mathematical language with computation rules developed by Per Martin-Löf. Type Theory was initially developed as a formalization of constructive mathematics but Martin-Löf has pointed out that it can also be viewed as a formal system for the development of provably correct programs. Here, a parser for a simple expression language is specified and a program derived from the proof of correctness of its specification using the formalism of Type Theory. The proof is compared with a proof of the same problem formalized in the Edinburgh LCF system.     

Deductive verification of alternating systems

Alternating systems are models of computer programs whose behavior is governed by the actions of multiple agents with, potentially, different goals. Examples include control systems, resource schedulers, security protocols, auctions and election mechanisms. Proving properties about such systems has emerged as an important new area of study in formal verification, with the development of logical frameworks such as the alternating temporal logic ATL*. Techniques for model checking ATL* over finite-state systems have been well studied, but many important systems are infinite-state and thus their verification requires, either explicitly or implicitly, some form of deductive reasoning. This paper presents a theoretical framework for the analysis of alternating infinite-state systems. It describes models of computation, of various degrees of generality, and alternating-time logics such as ATL* and its variations. It then develops a proof system that allows to prove arbitrary ATL* properties over these infinite-state models. The proof system is shown to be complete relative to validities in the weakest possible assertion language. The paper then derives auxiliary proof rules and verification diagrams techniques and applies them to security protocols, deriving a new formal proof of fairness of a multi-party contract signing protocol where the model of the protocol and of the properties contains both game-theoretic and infinite-state (parameterized) aspects.     

Unfolding-based Improvements on Fuzzy Logic Programs

Unfolding is a semantics-preserving program transformation technique that consists in the expansion of subexpressions of a program using their own definitions. In this paper we define two unfolding-based transformation rules that extend the classical definition of the unfolding rule (for pure logic programs) to a fuzzy logic setting. We use a fuzzy variant of Prolog where each program clause can be interpreted under a different (fuzzy) logic. We adapt the concept of a computation rule, a mapping that selects the subexpression of a goal involved in a computation step, and we prove the independence of the computation rule. We also define a basic transformation system and we demonstrate its strong correctness, that is, original and transformed programs compute the same fuzzy computed answers. Finally, we prove that our transformation rules always produce an improvement in the efficiency of the residual program, by reducing the length of successful Fuzzy SLD-derivations.     

命令的操作语义在类型系统中的一种表示

类型系统建立在一个小的规则集合基础上，易于实现，可理解性好，且具有计算完全性和足够的表达能力,在类型系统中可以重述推导规则，将其形式化为一些归纳关系，从而直接表示了命令的操作语义,类型理论不仅适合于函数式程序的证明，也是刻画和证明命令式程序的合适的框架。     

Proving weak properties of rewriting

In rule-based programming, properties of programs, such as termination, are in general considered in their strong acceptance, i.e., on every computation branch. But in practice, they may hold in their weak acceptance only, i.e., on at least one computation branch. Moreover, weak properties are often enough to ensure that programs give the expected result. There are very few results to handle weak properties of rewriting. We address here two of them: termination and reducibility to a constructor form, in a unified framework allowing us to prove them inductively. Proof trees are developed, which simulate rewriting trees by narrowing and abstracting subterms. Our technique is constructive in the sense that proof trees can be used to infer an evaluation strategy for any given input: the right computation branch is developed without using a costly breadth-first strategy nor backtracking.     

Focusing and polarization in linear,intuitionistic, and classical logics

A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. These focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system LKF for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard’s LC and LU proof systems.     

Static analysis of Linear Logic programming

Linear Logic is gaining momentum in computer science because it offers a unified framework and a common vocabulary for studying and analyzing different aspects of programming and computation. We focus here on models where computation is identified with proof search in the sequent system of Linear Logic. A proof normalization procedure, called “focusing”, has been proposed to make the problem of proof search tractable. Correspondingly, there is a normalization procedure mapping formulae of Linear Logic into a syntactic fragment of that logic, calledLinLog, where the focusing normalization for proofs can be most conveniently expressed. In this paper, we propose to push this compilation/normalization process further, by applying abstract interpretation and partial evaluation techniques to (focused) proofs inLinLog. These techniques provide information concerning the evolution of the computational resources (formulae) during the execution (proof construction). The practical outcome that we expect from this theoretical effort is the definition of a general tool for statically analyzing and reasoning about the runtime behavior of programs in frameworks where computations can be accounted for in terms of proof search in Linear Logic.     

Proof by consistency

Advances of the past decade in methods and computer programs for showing consistency of proof systems based on first-order equations have made it feasible, in some settings, to use proof by consistency as an alternative to conventional rules of inference. Musser described the method applied to proof of properties of inductively defined objects. Refinements of this inductionless induction method were discussed by Kapur, Goguen, Huet and Hullot, Huet and Oppen, Lankford, Dershowitz, Paul, and more recently by Jouannaud and Kounalis as well as by Kapur, Narendran and Zhang. This paper gives a very general account of proof by consistency and inductionless induction, and shows how previous results can be derived simply from the general theory. New results include a theorem giving characterizations of an unambiguity property that is key to applicability of proof by consistency, and a theorem similar to the Birkhoff's Completeness Theorem for equational proof systems, but concerning inductive proof.     

Adequate proof principles for invariance and liveness properties of concurrent programs

This paper presents proof principles for establishing invariance and liveness properties of concurrent programs. Invariance properties are established by systematically checking that they are preserved by every atomic instruction in the program. The methods for establishing liveness properties are based on well-founded assertions and are applicable to both ‘just’ and ‘fair’ computations. These methods do not assume a decrease of the rank at each computation step. It is sufficient that there exists one process which decreases the rank when activated. Fairness then ensures that the program will eventually attain its goal. In the finite state case such proofs can be represented by diagrams. Several examples are given.     

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     

Linear logic by levels and bounded time complexity

We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard’s seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratification, based on inducing levels in proof nets by means of indices, which allows us to extend Girard’s systems while keeping the same complexity properties. In particular, it turns out that Girard’s systems can be recovered by forcing depth and level to coincide. A consequence of the higher flexibility of levels with respect to depth is the absence of boxes for handling the paragraph modality. We use this fact to propose a variant of our polytime system in which the paragraph modality is only allowed on atoms, and which may thus serve as a basis for developing lambda-calculus type assignment systems with more efficient typing algorithms than existing ones.     

Best-order streaming model

We study a new model of computation, called best-order stream, for graph problems. Roughly, it is a proof system where a space-limited verifier has to verify a proof sequentially (i.e., it reads the proof as a stream). Moreover, the proof itself is just a specific ordering of the input data. This model is closely related to many models of computation in other areas such as data streams, communication complexity, and proof checking, and could be used in applications such as cloud computing.In this paper we focus on graph problems where the input is a sequence of edges. We show that even under this model, checking some basic graph properties deterministically requires linear space in the number of nodes. We also show that, in contrast with this, randomized verifiers are powerful enough to check many graph properties in polylogarithmic space.     

Lazy techniques for fully expansive theorem proving

The HOL system is afully expansive theorem prover: proofs generated in the system are composed of applications of the primitive inference rules of the underlying logic. One can have a high degree of confidence that such systems are sound, but they are far slower than theorem provers that exploit metatheoretic or derived properties.This paper presents techniques for postponing part of the computation so that the user of a fully expansive theorem prover can be more productive. The notions oflazy theorem andlazy conversion are introduced. These not only allow part of the computation to be delayed, but also permit nonlocal optimizations that are only possible because the primitive inferences are not performed immediately. The approach also opens the way to proof procedures that exploit metatheoretic properties without sacrificing security; the primitive inferences still have to be performed in order to generate a theorem, but during the proof development the user is free of the overheads they entail.     

Verification of distributed systems with local�Cglobal predicates

This paper describes a methodology for developing and verifying a class of distributed systems in which the state space may be discrete or continuous. Our focus is on systems where changes are local in that a small number of components change state while the remainder of the system is unchanged. A proof methodology is developed that ensures global properties, such as invariants and convergence, by guaranteeing local properties within subsystems. This methodology is used to prove the correctness of concrete examples. We present a PVS library of theorems and proofs that can be used to reduce the work required to develop and verify programs in this class. A transformation of these libraries to Java is also outlined.     

Proof rules and transformations dealing with fairness

We provide proof rules enabling the treatment of two fairness assumptions in the context of Dijkstra's do-od-programs. These proof rules are derived by considering a transformed version of the original program which uses random assignments z?? and admits only fair computations. Various, increasingly complicated, examples are discussed. In all cases reasonably simple proofs can be given. The proof rules use well-founded structures corresponding to infinite ordinals and deal with the original programs and not their translated versions.     

A verification system for concurrent programs based on the Boyer-Moore prover

We describe a mechanical proof system for concurrent programs, based on a formalization of the temporal framework of Manna and Pnueli as an extension of the computational logic of Boyer and Moore. The system provides a natural representation of specifications of concurrent programs as temporal logic formulas, which are automatically translated into terms that are subject to verification by the Boyer-Moore prover. Several specialized derived rules of inference are introduced to the prover in order to facilitate the verification of invariance (safety) and eventuality (liveness) properties. The utility of the system is illustrated by a correctness proof for a two-process program that computes binomial coefficients.     

模型转换中特性保持的描述与验证

模型转换主要用于模型的演化、求精以及重构.模型转换需要遵循一定的约束规则以保持模型的某些特性.模型演化通常要求保持已有的接口;模型重构则必须保证重构前后的软件具有相同的外部行为特性.为了严格证明某个模型转换规则是否满足这些约束,特性保持约束必须形式化地加以描述.为了实现证明过程的自动化,需要总结通用的证明过程并给出实现算法.提出了一种基于图转换的特性保持约束描述机制,将模型演化与重构中的转换规则以及特性保持约束都描述为图转换规则.借助图转换的冲突检测机制,给出了严格证明转换规则是否满足特性保持约束的算法.     

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.