Nondeterministic flowchart programs with recursive procedures: Semantics and correctness II

In the second part of this work, we formulate a new inductive assertion method applying to the class of nondeterministic flowchart programs with recursive procedures studied in part 1. Using results on unfolding proved in part 1, we prove that this method is sound and complete with a finite number of assertions. We study four notions of correctness: two notions of partial correctness (existential and universal) and the corresponding notions of total correctness. We also formalize two notions of extension and equivalence (existential and universal) in the second-order predicate calculus.     

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     

Frame rule for mutually recursive procedures manipulating pointers

Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove a powerful Hoare total correctness rule for mutually recursive procedures manipulating pointers. The rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. The theory, including the proofs, is implemented in the theorem prover PVS. In this implementation program variables and addresses can store values of almost any type of the theorem prover.     

Kleene under a modal demonic star

In relational semantics, the input-output semantics of a program is a relation on its set of states. We generalise this in considering elements of Kleene algebras as semantical values. In a nondeterministic context, the demonic semantics is calculated by considering the worst behaviour of the program. In this paper, we concentrate on while loops. Calculating the semantics of a loop is difficult, but showing the correctness of any candidate abstraction is much easier. For deterministic programs, Mills has described a checking method known as the while statement verification rule. A corresponding programming theorem for nondeterministic iterative constructs is proposed, proved and applied to an example. This theorem can be considered as a generalisation of the while statement verification rule to nondeterministic loops. The paper generalises earlier relation-algebraic work to the setting of modal Kleene algebra, an extension of Kozen’s Kleene algebra with tests that allows the internalisation of weakest liberal precondition and strongest liberal postcondition operators.     

Programs as partial graphs II: Recursion

In Part I of the paper, we have proposed a unified relational algebra approach using partial graphs for theoretical investigations on semantics, correctness and termination. This approach is extended here to systems of recursive programs, allowing not only sequencing and conditional branching as a control structure but also flow diagrams.An equivalence proof of operational and denotational semantics is obtained which is strictly based on axioms of relational algebra. A short new proof of an important completeness result is given in the generalized setting of systems of recursive flow diagram programs. Finally, Hitchcock-Park's theorem on derivatives is formulated in the general case of nondeterministic recursive flow diagram programs.     

Goto and Concurrency Introducing Safe Jumps in Esterel

Esterel is a design language for the specification of real time embedded systems. Based on the synchronous concurrency paradigm, its semantics describes execution as a succession of instants of computation. In this work, we consider the introduction of a new gotopause instruction in the language, which acts as a non-instantaneous jump instruction compatible with concurrency. It allows the programmer to activate state control points anywhere in the program, from where the execution is resumed in the next instant. In order to provide the formal semantics of the extended language, we first define a state semantics of Esterel, which we prove observationally equivalent to the original logical behavioral semantics. Including gotopause in the state semantics is then straightforward. We sketch two key applications of our new primitive: a direct encoding of automata and a quasi-linear rewriting of programs eliminating schizophrenic behaviors.     

Towards an efficient evaluation of recursive aggregates in deductive databases

This paper is devoted to the evaluation of aggregates (avg, sum,…) in deductive databases. Aggregates have proved to be a necessary modeling tool for a wide range of applications in non-deductive relational databases. They also appear to be important in connection with recursive rules, as shown by thebill of materials example. Several recent papers have studied the problem of semantics for aggregate programs. As in these papers, we distinguish between the classes of stratified (non-recursive) and recursive aggregate programs. For each of these two classes, the declarative semantics is recalled and an efficient evaluation algorithm is presented. The semantics and computation of aggregate programs in the recursive case are more complex: we rely on the notion of graph traversal to motivate the semantics and the evaluation method proposed. The algorithms presented here are integrated in the QSQ framework. Our work extends the recent work on aggregates by proposing an efficient algorithm in the recursive case. Recursive aggregates have been implemented in the EKS-V1 system.     

On the autoepistemic reconstruction of logic programming

Current semantics of logic programs normally ignore thesyntactical aspects of the programs. As a result, only the meanings ofsome well-behaved programs can be captured by these semantics. In this paper however, we propose a new semantics of logic programs that can reflectsome of the syntactical behaviours of the programs. The central notion of the semantics is the concept of aneutral clause p ← A which does not affect the behaviour of p in a program. The logic that underlies the semantics is based on anintensional extension of Levesque’s autoepistemicpredicate logic. It differs from existing autoepistemic logics in that it isquantificational andconstructive. We will also compare and contrast our semantics with some well-known semantics. In particular, we will show how to capture the undefined value of a logic program without resorting to a three-valued nonmonotonic formalism. This is achieved by translating an incoherent AE logic program to a program with multiple AE extensions whose intersection can then be used to characterize the undefined value of a logic program.     

指令级并行程序执行模型

提出了一种形式化的指令级并行程序执行模型,ＩＬＰＰＥＭ不仅可以描述程序实际执行过程的行为,也可以描述编译和执行时不确定的时间变化所造成的可行执行过程的行为;同时提出了程序执行的同构概念,并证明了可行程序执行必与一个实际程序执行同构,从而为并行程序编译和验证提供了理论依据。     

A survey of new trends in symbolic execution for software testing and analysis

Symbolic execution is a well-known program analysis technique which represents program inputs with symbolic values instead of concrete, initialized, data and executes the program by manipulating program expressions involving the symbolic values. Symbolic execution has been proposed over three decades ago but recently it has found renewed interest in the research community, due in part to the progress in decision procedures, availability of powerful computers and new algorithmic developments. We provide here a survey of some of the new research trends in symbolic execution, with particular emphasis on applications to test generation and program analysis. We first describe an approach that handles complex programming constructs such as input recursive data structures, arrays, as well as multithreading. Furthermore, we describe recent hybrid techniques that combine concrete and symbolic execution to overcome some of the inherent limitations of symbolic execution, such as handling native code or availability of decision procedures for the application domain. We follow with a discussion of techniques that can be used to limit the (possibly infinite) number of symbolic configurations that need to be analyzed for the symbolic execution of looping programs. Finally, we give a short survey of interesting new applications, such as predictive testing, invariant inference, program repair, analysis of parallel numerical programs and differential symbolic execution.     

Logic programming with solution preferences

Preference logic programming (PLP) is an extension of logic programming for declaratively specifying problems requiring optimization or comparison and selection among alternative solutions to a query. PLP essentially separates the programming of a problem itself from the criteria specification of its solution selection. In this paper we present a declarative method for specifying preference logic programs. The method introduces a precise formalization for the syntax and semantics of PLP. The syntax of a preference logic program contains two disjoint sets of definite clauses, separating a core program specifying a general computational problem from its preference rules for optimization; the semantics of PLP is given based on the Herbrand model and fixed point theory, where how preferences affects the least Herbrand model of a logic program is interpreted as a sequence of meta-level mapping operations. In addition, we present an operational semantics based on a new resolution strategy and a memoized recursive algorithm for computing strictly stratified logic programs with well-formed preferences, and further show that the operational semantics of such a preference logic program is consistent to its declarative semantics.     

AgentSpeak中意图生成过程的可靠性与完整性研究

意图生成是BDI型Agent为实现目标而产生动作序列的过程。验证软件Agent中意图生成的正确性是Agent编程语言中一个重要的研究问题。针对软件Agent中意图执行的正确性,以当前最流行的BDI型Agent编程语言AgentSpeak为例,证明了软件Agent意图执行的有效性。首先根据AgentSpeak的语法构造了一个解释系统,并给出了该解释系统的满足关系,从而得出了AgentSpcak的模型论语义。在该模型论语义的基础上,结合由Moreira和Bordini所给出的操作语义,证明了AgentSpeak的意图生成等价定理:AgentSpeak语言中模型论语义的意图等价于AgentSpeak程序操作语义的意图。由此可得出结论—AgentSpcak中的意图执行是可靠而完整的,从而验证了AgcntSpcak中软件Agent意图完成目标的正确性。     

Termination of nondeterministic quantum programs

We define a language-independent model of nondeterministic quantum programs in which a quantum program consists of a finite set of quantum processes. These processes are represented by quantum Markov chains over the common state space, which formalize the quantum mechanical behaviors of the machine. An execution of a nondeterministic quantum program is modeled by a sequence of actions of individual processes, and at each step of an execution a process is chosen nondeterministically to perform the next action. This execution model formalize the users’ behavior of calling the processes in the classical world. Applying the model to a quantum walk as an instance of physically realizable systems, we describe an execution step by step. A characterization of reachable space and a characterization of diverging states of a nondeterministic quantum program are presented. We establish a zero-one law for termination probability of the states in the reachable space. A combination of these results leads to a necessary and sufficient condition for termination of nondeterministic quantum programs. Based on this condition, an algorithm is found for checking termination of nondeterministic quantum programs within a fixed finite-dimensional state space.     

A Standard Model—Theoretic Approach to Operational Semmantics of Recursiv Programs

In this paper we try to introduce a new approach to operational semantics of recursive programs by using ideas in the“priority method”which is a fundamental tool in Recursion Theory.In lieu of modelling partial functions by introducing undefined values in a traditional approach,we shall define a priority derivation tree for every term,and by respecting thr rule“attacking the subtem of the highest priority first”we define transition relations,computation sequences etc.directly based on a standard interpretation whic includes no undefined value in its domain,Finally,we prove that our new approach generates the same opeational semantics as the traditional one.It is also pointed out that we can use our strategy oto refute a claim of Loeckx and Sieber that the opperational semantics of recursive programs cannot be built based on predicate logic.     

Execution levels for aspect-oriented programming: Design,semantics, implementations and applications

In aspect-oriented programming (AOP) languages, advice evaluation is usually considered as part of the base program evaluation. This is also the case for certain pointcuts, such as if pointcuts in AspectJ, or simply all pointcuts in higher-order aspect languages like AspectScheme. While viewing aspects as part of base level computation clearly distinguishes AOP from reflection, it also comes at a price: because aspects observe base level computation, evaluating pointcuts and advice at the base level can trigger infinite regression. To avoid these pitfalls, aspect languages propose ad-hoc mechanisms, which increase the complexity for programmers while being insufficient in many cases. After shedding light on the many facets of the issue, this paper proposes to clarify the situation by introducing levels of execution in the programming language, thereby allowing aspects to observe and run at specific, possibly different, levels. We adopt a defensive default that avoids infinite regression, and gives advanced programmers the means to override this default using level-shifting operators. We then study execution levels both in practice and in theory. First, we study the relevance of the issues addressed by execution levels in existing aspect-oriented programs. We then formalize the semantics of execution levels and prove that the default semantics is indeed free of a certain form of infinite regression, which we call aspect loops. Finally, we report on existing implementations of execution levels for aspect-oriented extensions of Scheme, JavaScript and Java, discussing their implementation techniques and current applications.     

A continuous semantics for unbounded nondeterminism

Nondeterminism is introduced into an ordinary iterative programming language by treating procedure calls as nondeterministic assignment statements. The effect of such assignment statements is assumed to be determined solely by the entry-exit specifications of the corresponding procedures. The nondeterminism which this approach yields is not necessarily bounded. The paper discusses the problem of defining a denotational semantic for programming languages with this kind of, possibly unbounded, nondeterminism. As an additional constraint, the semantics is required to be continuous, in the sense that the underlying semantic algebra is continuous. It is shown how such a continuous semantics for unbounded nondeterminism can be derived from a simple operational semantics based on program execution trees.     

Relational semantics for locally nondeterministic programs

Introducing nondeterministic operators in a conventional deterministic language gives rise to various semantic difficulties. One of the problems is that there has been no semantic domain that is wholly satisfactory for denoting nondeterministic programs. In this paper, we propose an approach based on relational algebra. We divide the semantics of a nondeterministic program into two parts. The first part concerns the angelic aspect of programs and the second part concerns the demonic aspect of programs. Because each semantic function used in these parts is monotonic with respect to an ordering on relations, the existence of the fixed points of recursively defined nondeterministic programs is ensured. Liangwei Xu: His research interests are computational model, program transformation and derivation methodology. He received the B. E. degree from Shanghai Jiao Tong University in 1982 and the M.E. degree from University of Tokyo in 1992. He currently joins Mathematical Systems Institute Inc. Masato Takeichi, Dr. Eng.: He is a Professor of Department of Mathematical Engineering. Graduate School of Engineering, University of Tokyo. His research interests are functional programming, language implementation and constructive algorithmics. Hideya Iwasaki, Dr. Eng.: He is an Associate Professor of Faculty of Technology, Tokyo University of Agriculture and Technology. He received the M.E. degree in 1985, the Dr. Eng. degree in 1988 from University of Tokyo. His research interests are list processing languages, functional languages, parallel processing, and constructive algorithmics.     

OR-parallel evaluation of logic programs on a multi-ring dataflow machine

Logic programming languages have gained wide acceptance because of two reasons. First is their clear declarative semantics and the second is the wide scope for parallelism they provide which can be exploited by building suitable parallel architectures. In this paper, we propose a multi-ring dataflow machine to support theOR-parallelism and theArgument parallelism of logic programs. A new scheme is suggested for handling the deferred read mechanism of the dataflow architecture. The required data structures, the dataflow actors and the builtin dataflow procedures for OR-parallel execution are discussed. Multiple binding environments arising in the OR-parallel execution are handled by a new scheme called thetagged variable scheme. Schemes for constrained OR-parallel execution are also discussed.     

Command algebras,recursion and program transformation

Dijkstra's language of guarded commands is extended with recursion and transformed into algebra. The semantics is expressed in terms of weakest preconditions and weakest liberal preconditions. Extreme fixed points are used to deal with recursion. Unbounded nondeterminacy is allowed. The algebraic setting enables us to develop efficient transformation rules for recursive procedures. The main result is an algebraic version of the rule of computational induction. In this version, certain parts of the programs are restricted to finite nondeterminacy. It is shown that without this restriction the rule would not be valid. Some applications of the rule are presented. In particular, we prove the correctness of an iterative stack implementation of a class of simple recursive procedures.