Beyond multi-adjoint logic programming

In ‘multi-adjoint logic programming’, MALP in brief, each fuzzy logic program is associated with its own ‘multi-adjoint lattice’ for modelling truth degrees beyond the simpler case of true and false, where a large set of fuzzy connectives can be defined. On this wide repertoire, it is crucial to connect each implication symbol with a proper conjunction thus conforming constructs of the form (←_i, &_i) called ‘adjoint pairs’, whose use directly affects both declarative and operational semantics of the MALP framework. In this work, we firstly show how the strong dependence of adjoint pairs can be largely weakened for an interesting ‘sub-class’ of MALP programs. Then, we reason in a similar way till conceiving a ‘super-class’ of fuzzy logic programs beyond MALP, which definitively drops out the need for using adjoint pairs, since the new semantics behaviour relies on much more relaxed lattices than multi-adjoint ones.     

Mixed computation: potential applications and problems for study

Mixed computation is processing of an incomplete information. Its product are a partially processed information and a so-called residual program destined to complete in sequel the processing of the remaining information. Many kinds of practical work with programs are nothing more but obtaining a residual program. We demonstrate, as an example, the application of mixed computation to compilation. Under computational approach mixed computation generalizes the operational semantics of a language by inclusion of steps which generate residual program instructions. Under transformational approach the residual program is obtained as a result of a series of so-called basic transformations of the program text. We argue that the transformational approach is more fundamental, for it allows to describe mixed computation in all its variety and moreover, to relate mixed computation to other kinds of program manipulation: execution, optimization, macroprocessing, synthesis. Such an integrated approach leads us to a transformational machine concept.     

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

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

Nondeterministic flowchart programs with recursive procedures: semantics and correctness I

In this paper, we study some aspects of the semantics of nondeterministic flowchart programs with recursive procedures. In the first part of this work we provide the operational semantics of programs using the concept of an execution tree. We propose a new definition of the semantics of a non-deterministic recursive program as a mapping from the input domain to the set of execution trees determined by the program. Using this new concept, we prove that every nondeterministic flowchart program with recursive procedures can be unfolded into a semantically equivalent infinite pure flowchart (without procedures). This result is applied in the second part of this work to prove the soundness of an inductive assertion method which is also complete with a finite number of assertions (contrary to De Bakker and Meertens's method [11]).     

Abstract interpretation of resolution-based semantics

We extend the abstract interpretation point of view on context-free grammars by Cousot and Cousot to resolution-based logic programs and proof systems. Starting from a transition-based small-step operational semantics of Prolog programs (akin to the Warren Machine), we consider maximal finite derivations for the transition system from most general goals. This semantics is abstracted by instantiation to terms and furthermore to ground terms, following the so-called c- and s-semantics approach. Orthogonally, these sets of derivations can be abstracted to SLD-trees, call patterns and models, as well as interpreters providing effective implementations (such as Prolog). These semantics can be presented in bottom–up fixpoint form. This abstract interpretation-based construction leads to classical bottom–up semantics (such as the s-semantics of computed answers, the c-semantics of correct answers of Keith Clark, and the minimal-model semantics of logical consequences of Maarten van Emden and Robert Kowalski). The approach is general and can be applied to infinite and top–down semantics in a straightforward way.     

Inductive assertions and operational semantics

This paper shows how classic inductive assertions can be used in conjunction with a formal operational semantics to prove partial correctness properties of programs. The method imposes only the proof obligations that would be produced by a verification condition generator – but does not require the definition of a verification condition generator. All that is required is a theorem prover, a formal operational semantics, and the object program with appropriate assertions at user-selected cut points. The verification conditions are generated in the course of the theorem-proving process by straightforward symbolic evaluation of the formal operational semantics. The technique is demonstrated by proving the partial correctness of simple bytecode programs with respect to a preexisting operational model of the Java Virtual Machine.     

Nested expressions in logic programs

We extend the answer set semantics to a class of logic programs with nested expressions permitted in the bodies and heads of rules. These expressions are formed from literals using negation as failure, conjunction (,) and disjunction (;) that can be nested arbitrarily. Conditional expressions are introduced as abbreviations. The study of equivalent transformations of programs with nested expressions shows that any such program is equivalent to a set of disjunctive rules, possibly with negation as failure in the heads. The generalized answer set semantics is related to the Lloyd–Topor generalization of Clark’s completion and to the logic of minimal belief and negation as failure. This revised version was published online in June 2006 with corrections to the Cover Date.     

Tor: Modular search with hookable disjunction

Horn Clause Programs have a natural exhaustive depth-first procedural semantics. However, for many programs this semantics is ineffective. In order to compute useful solutions, one needs the ability to modify the search method that explores the alternative execution branches.Tor, a well-defined hook into Prolog disjunction, provides this ability. It is light-weight thanks to its library approach and efficient because it is based on program transformation. Tor  is general enough to mimic search-modifying predicates like ECLiPSe’s search/6. Moreover, Tor  supports modular composition of search methods and other hooks. The Tor  library is already provided and used as an add-on to SWI-Prolog.     

Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language

Complex software systems typically involve features like time, concurrency and probability, with probabilistic computations playing an increasing role. However, it is currently challenging to formalize languages incorporating all those features. Recently, the language PTSC has been proposed to integrate probability and time with shared-variable concurrency (Zhu et al. (2006, 2009) [51] and [53]), where the operational semantics has been explored and a set of algebraic laws has been investigated via bisimulation. This paper investigates the link between the operational and algebraic semantics of PTSC, highlighting both its theoretical and practical aspects.The link is obtained by deriving the operational semantics from the algebraic semantics, an approach that may be understood as establishing soundness of the operational semantics with respect to the algebraic semantics. Algebraic laws are provided that suffice to convert any PTSC program into a form consisting of a guarded choice or an internal choice between programs, which are initially deterministic. That form corresponds to a simple execution of the program, so it is used as a basis for an operational semantics. In that way, the operational semantics is derived from the algebraic semantics, with transition rules resulting from the derivation strategy. In fact the derived transition rules and the derivation strategy are shown to be equivalent, which may be understood as establishing completeness of the operational semantics with respect to the algebraic semantics.That theoretical approach to the link is complemented by a practical one, which animates the link using Prolog. The link between the two semantics proceeds via head normal form. Firstly, the generation of head normal form is explored, in particular animating the expansion laws for probabilistic interleaving. Then the derivation of the operational semantics is animated using a strategy that exploits head normal form. The operational semantics is also animated. These animations, which again supports to claim soundness and completeness of the operational semantics with respect to the algebraic, are interesting because they provide a practical demonstration of the theoretical results.     

Linear Approximation of Execution-Time Constraints

This paper defines an algorithm for predicting worst-case and best-case execution times, and determining execution-time constraints of control-flow paths through real-time programs using their partial correctness semantics. The algorithm produces a linear approximation of path traversal conditions, worst-case and best-case execution times and strongest postconditions for timed paths in abstract real-time programs. Also shown are techniques for determining the set of control-flow paths with decidable worst-case and best-case execution times. The approach is based on a weakest liberal precondition semantics and relies on supremum and infimum calculations similar to standard computations from linear programming and Presburger arithmetic. The methodology is applicable to any executable language with a predicate transformer semantics and hence provides a verification basis for both high-level language and assembly code execution-time analysis.     

Bi-inductive Structural Semantics: (Extended Abstract)

We propose a simple order-theoretic generalization of set-theoretic inductive definitions. This generalization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows the structural operational semantics to describe simultaneously the finite/terminating and infinite/diverging behaviors of programs. This is illustrated on the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value λ-calculus.     

基于函数式语义的循环和递归程序结构通用证明技术

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.     

Magic-sets for localised analysis of Java bytecode

Static analyses based on denotational semantics can naturally model functional behaviours of the code in a compositional and completely context and flow sensitive way. But they only model the functional i.e., input/output behaviour of a program P, not enough if one needs P’s internal behaviours i.e., from the input to some internal program points. This is, however, a frequent requirement for a useful static analysis. In this paper, we overcome this limitation, for the case of mono-threaded Java bytecode, with a technique used up to now for logic programs only. Namely, we define a program transformation that adds new magic blocks of code to the program P, whose functional behaviours are the internal behaviours of P. We prove the transformation correct w.r.t. an operational semantics and define an equivalent denotational semantics, devised for abstract interpretation, whose denotations for the magic blocks are hence the internal behaviours of P. We implement our transformation and instantiate it with abstract domains modelling sharing of two variables, non-cyclicity of variables, nullness of variables, class initialisation information and size of the values bound to program variables. We get a static analyser for full mono-threaded Java bytecode that is faster and scales better than another operational pair-sharing analyser. It has the same speed but is more precise than a constraint-based nullness analyser. It makes a polyhedral size analysis of Java bytecode scale up to 1300 methods in a couple of minutes and a zone-based size analysis scale to still larger applications.     

S-semantics for logic programming: A retrospective look

The paper provides an overview of the s-semantic approach to the semantics of logic programs which had been developed about twenty years ago. The aim of such an approach was that of providing a suitable base for program analysis by means of a semantics which really captures the operational behavior of logic programs, and thus offers useful notions of observable program equivalences. The semantics is given in terms of extended interpretations, which are more expressive than Herbrand interpretations, extends the standard Herbrand semantics, and can be obtained as a result of both top-down and bottom-up constructions. The approach has been applied to several extensions of positive logic programs and used to develop semantic-based techniques for program analysis, verification and transformation.     

Term Rewriting with Type-safe Traversal Functions

Term rewriting is an appealing technique for performing program analysis and program transformation. Tree (term) traversal is frequently used but is not supported by standard term rewriting. In this paper, many-sorted first-order term rewriting is extended with automatic tree traversal by adding two primitive tree traversal strategies and complementing them with three types of traversals. These so-called traversal functions can be either top-down or bottom-up. They can be sort preserving, mapping to a single sort, or a combination of these two. Traversal functions have a simple design, their application is type-safe in a first-order many-sorted setting and can be implemented efficiently. We describe the operational semantics of traversal functions and discuss applications.     

On Probabilistic Techniques for Data Flow Analysis

We present a semantics-based technique for analysing probabilistic properties of imperative programs. This consists in a probabilistic version of classical data flow analysis. We apply this technique to pWhile programs, i.e programs written in a probabilistic version of a simple While language. As a first step we introduce a syntax based definition of a linear operator semantics (LOS) which is equivalent to the standard structural operational semantics of While. The LOS of a pWhile program can be seen as the generator of a Discrete Time Markov Chain and plays a similar role as a collecting or trace semantics for classical While. Probabilistic Abstract Interpretation techniques are then employed in order to define data flow analyses for properties like Parity and Live Variables.     

进程创建的语义及等价性

针对一个基于共享变量的带有进程创建的命令式语言,用变迁系统描述了它的结构操作语义,并用扩展的状态变迁迹模型定义了它的指称语义,在该模型下,状态变迁被区分为两种不同形式,分别表示发生在原进程和被创建进程中的状态变迁,这样便可以定义适当的语义复合运算,在对命令的指称进行复合时根据变迁类型的不同对变迁迹进行串行或交错连接,恰当地反映了进程的并发运行受创建命令在程序中的相对位置的限制,最后证明了这两个语义     

Online efficient predictive safety analysis of multithreaded programs

We present an automated and configurable technique for runtime safety analysis of multithreaded programs that is able to predict safety violations from successful executions. Based on a formal specification of safety properties provided by a user, our technique enables us to automatically instrument a given program and create an observer so that the program emits relevant state update events to the observer and the observer checks these updates against the safety specification. The events are stamped with dynamic vector clocks, enabling the observer to infer a causal partial order on the state updates. All event traces that are consistent with this partial order, including the actual execution trace, are then analyzed online and in parallel. A warning is issued whenever one of these potential traces violates the specification. Our technique is scalable and can provide better coverage than conventional testing, but its coverage need not be exhaustive. In fact, one can trade off scalability and comprehensiveness: a window in the state space may be specified allowing the observer to infer some of the more likely runs; if the size of the window is 1, then only the actual execution trace is analyzed, as is the case in conventional testing; if the size of the window is ∞, then all the execution traces consistent with the actual execution trace are analyzed.     

A formal semantics for debugging synchronous message passing-based concurrent programs

In this paper, we propose a semantic framework to debug synchronous message passing-based con- current programs, which are increasingly useful as parallel computing and distributed systems become more and more pervasive. We first design a concurrent programming language model to uniformly represent exist- ing concurrent programming languages. Compared to sequential programming languages, this model contains communication statements, i.e., sending and receiving statements, and a concurrent structure to represent com- munication and concurrency. We then propose a debugging process consisting of a tracing and a locating procedure. The tracing procedure re-executes a program with a failed test case and uses specially designed data structures to collect useful execution information for locating bugs. We provide for the tracing procedure a struc- tural operational semantics to represent synchronous communication and concurrency. The locating procedure backward locates the ill-designed statement by using information obtained in the tracing procedure, generates a fix equation, and tries to fix the bug by solving the fix equation. We also propose a structural operational semantics for the locating procedure. We supply two examples to test our proposed operational semantics.     

Verilog代数语义研究

给出了Verilog的代数语义.这是一个等式公理体系,它将Verilog语义特征通过代数规则简洁而准确地表达出来;并且这个代数语义相对于已经所作的操作语义模型来讲是可靠的,即所有的这些代数规则左右两边的进程在操作语义的观察模型下都是互模拟的.研究了此代数语义的相对完备性,即参照前面的操作语义模型,相对于扩展Verilog语言的一个子集而言,此代数语义是完备的.即所有符合这样语法的程序,如果它们是互模拟等价的,那么它们同样可以在所提出的代数系统中被推导相等.在完备性证明过程中,采用范式方法,即构造一种语法上特殊的程序,任何属于上述子集中的一个程序通过该代数规则都能够被转化为范式程序,而且范式程序在操作语义模型下是互模拟的当且仅当它们是语法相同的.上述结果具有重要的理论意义,因为现有的进程代数理论主要是针对管道通信并行语言而展开的,而对于像Verilog这种以共享变量通信为基础的复杂并行语言研究还是比较少的,对此类复杂的基于共享变量的并行语言的进程代数理论研究提出了一种通用、有效的方法.