Goto elimination in program algebra

This paper shows that program algebra (PGA) [J.A. Bergstra, M.E. Loots, Program algebra for sequential code, J. Logic Algebraic Programm. 51 (2002) 125–156] offers a mathematical and systematic framework for reasoning about correctness and equivalence of algorithms and transformation rules for goto removal. We study correctness and equivalence for the algorithm proposed by Cooper for goto elimination with additional boolean variables. To remove goto statements without the use of additional variables, we propose a technique to get rid of head-to-head crossings and subsequently employ the results of Peterson et al. and Ramshaw. Finally, we provide formal correctness proofs in the setting of PGA for industrial transformation rules given recently by Veerman for restructuring Cobol programs in real-life applications. We hereby show that PGA can explain goto elimination with mathematical rigor to a larger public.     

A Transformational Derivation of a Parsing Algorithm in a High-Level Language

This paper presents a detailed algorithm derivation scenario, using correctness preserving source-to-source transfonnations. The algorithm derived is the Cocke-Younger nodal spans parsing algorithm. We describe a high-level SETL-like specification language, and give a partial correctness formalism and a set of transformation rules which enable the combination of algorithms whose partial correctness has already been established.     

A transformation system for concurrent processes

Program transformation techniques have been extensively studied in the framework of functional and logic languages, where they were applied mainly to obtain more efficient and readable programs. All these works are based on the Unfold/Fold program transformation method developed by Burstall and Darlington in the context of their recursive equational language. The use of Unfold/Fold based transformations for concurrent languages is a relevant issue that has not yet received an adequate attention. In this paper we define a transformation methodology for CCS. We give a set of general rules which are a specialization of classical program transformation rules, such as Fold and Unfold. Moreover, we define the general form of other rules, “oriented” to the goal of a transformation strategy, and we give conditions for the correctness of these rules. We prove that a strategy using the general rules and a set of goal oriented rules is sound, i.e. it transforms CCS programs into equivalent ones. We show an example of application of our method. We define a strategy to transform, if possible, a full CCS program into an equivalent program whose semantics is a finite transition system. We show that, by means of our methodology, we are able to a find finite representations for a class of CCS programs which is larger than the ones handled by the other existing methods. Our transformational approach can be seen as unifying in a common framework a set of different techniques of program analysis. A further advantage of our approach is that it is based only on syntactic transformations, thus it does not requires any semantic information. Received: 24 April 1997 / 19 November 1997     

过程式语言到函数式语言的抽象方法

本文给出了从过程式程序到函数式程序的转换规则，这些转换规则是从语言的接续指称语义推导出来的，我们考虑了ＧＯＴＯ语句的处理，因此，我们的方法可以处理非结构化程序。由于这些转换规则是从指称语义导出的，其正确性得到了保证。     

Behavior-Preserving Simulation-to-Animation Model and Rule Transformations

In the framework of graph transformation, simulation rules define the operational behavior of visual models. Moreover, it has been shown already how to construct animation rules from simulation rules by so-called S2A-transformation. In contrast to simulation rules, animation rules use symbols representing entities from the application domain in a user-oriented visualization. Using animation views for model execution provides better insights of model behavior to users, leading to an earlier detection of model inconsistencies. Hence, an important requirement of the animation view construction is the preservation of the behavior of the original visual model. This means, we have to show on the one hand semantical correctness of the S2A-transformation, and, on the other hand, semantical correctness of a suitable backwards-transformation A2S. Semantical correctness of a model and rule transformation means that for each sequence of the source system we find a corresponding sequence in the target system. S2A-transformation has been considered in our contribution to GraMoT 2006. In this paper, we give a precise definition for animation-to-simulation (A2S) backward transformation, and show under which conditions semantical correctness of an A2S backward transformation can be obtained. The main result states the conditions for S2A-transformations to be behavior-preserving. The result is applied to analyze the behavior of a Radio Clock model's S2A-transformation.     

A UML/OCL framework for the analysis of graph transformation rules

In this paper we present an approach for the analysis of graph transformation rules based on an intermediate OCL representation. We translate different rule semantics into OCL, together with the properties of interest (like rule applicability, conflicts or independence). The intermediate representation serves three purposes: (1) it allows the seamless integration of graph transformation rules with the MOF and OCL standards, and enables taking the meta-model and its OCL constraints (i.e. well-formedness rules) into account when verifying the correctness of the rules; (2) it permits the interoperability of graph transformation concepts with a number of standards-based model-driven development tools; and (3) it makes available a plethora of OCL tools to actually perform the rule analysis. This approach is especially useful to analyse the operational semantics of Domain Specific Visual Languages. We have automated these ideas by providing designers with tools for the graphical specification and analysis of graph transformation rules, including a back-annotation mechanism that presents the analysis results in terms of the original language notation.     

Algebraic reasoning for probabilistic action systems and while-loops

Back and von Wright have developed algebraic laws for reasoning about loops in a total correctness framework using the refinement calculus. We extend their work to reasoning about probabilistic loops in the probabilistic refinement calculus. We apply our algebraic reasoning to derive transformation rules for probabilistic action systems and probabilistic while-loops. In particular we focus on developing data refinement rules for these two constructs. Our extension is interesting since some well known transformation rules that are applicable to standard programs are not applicable to probabilistic ones: we identify some of these important differences and we develop alternative rules where possible.     

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.     

模型转换规则自动生成研究

在大规模的模型驱动工程中,模型转换是关键的环节,手动撰写模型转换规则既耗费资源,且正确性亦难以得到保障。针对该问题,提出基于编辑距离的模型比对算法,用于自动生成转换规则,该算法可以处理UML类图、状态图和活动图,而且可以有效地检测模型转移和复制操作,从而生成最小转换序列,提高模型转换工作效率。经过实验验证,基于该算法的模型转换规则自动生成方法是行之有效的。     

基于QVT的模型转换方法研究

针对不同模式之间规则不能重用甚至无法描述嵌套模式的问题．提出一种基于扩展MOF元模型与扩展QVT语言相结合的模型转换方法。该方法通过扩展MOF元模型解决模型之间规则不能重用问题．通过扩展QVTRelations可以增强规则语言的有效性,为模型建立和模型转换提供一种更有效的途径。在一个股票交易系统的转换应用实例中验证该方法的正确性。     

Estimating the concentration of optically active constituents of sea water by Takagi-Sugeno models with quadratic rule consequents

Determining the concentrations of chlorophyll, suspended particulate matter and coloured dissolved organic matter in the sea water is basic to support the monitoring of upwelling phenomena, algae blooms, and changes in the marine ecosystem. Since these concentrations affect the spectral distribution of the solar light back-scattered by the water body, their estimation can be computed by using a set of remotely sensed multispectral measurements of the reflected sunlight. In this paper, the relation between the concentrations of interest and the average subsurface reflectances is modelled by means of a set of second-order Takagi-Sugeno (TS) fuzzy rules. Unlike first-order TS rules, which adopt linear functions as consequent, second-order TS rules exploit quadratic functions, thus improving the modelling capability of the rule in the subspace determined by the antecedent. First, we show how we can build a second-order TS model through a simple transformation, which allows estimating the consequent parameters using standard linear least-squares algorithms, and by adopting one of the most used methods proposed in the literature to generate first-order TS models. Then, we compare first-order and second-order TS models against mean square error and interpretability of rules. We highlight how second-order TS models allow us to achieve better approximation than first-order TS models though maintaining interpretability of the rules. Finally, we show how second-order TS models perform considerably better (the mean square error is lower by two orders of magnitude) than the specific implementations of radial basis function networks and multi-layer perceptron networks used in previous papers for the same application domain.     

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.     

支持抽象解释的静态分析方法的形式化体系研究

在安全关键领域中,如何保证软件的安全性已经成为了一个广受关注的重要课题。静态程序分析是一类十分有效的程序自动化验证方法。基于抽象解释的静态分析技术在验证软件的非功能性安全属性上表现十分突出。可配置程序分析(Configurable Program Analysis,CPA)是一种通用静态分析方法形式化体系,旨在用一种形式化体系对静态分析的分析阶段进行建模。使用CPA对基于抽象解释的静态分析进行建模,给出如何使用CPA形式化体系描述基于抽象解释的静态分析,给出了从待分析程序到CPA形式化体系的转换规则;提供了一种在安全关键性领域中的软件正确性自动验证方法,为基于抽象解释的静态分析工具的实现提供了一种可行方案。     

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.     

基于CPN的求解关键路径的新方法

在证明转换规则正确性的基础上,首先利用转换规则对 AOE 网进行转换,然后从两个方面对转换后的CPN(Colored Petri Nets)模型不合理的地方进行合理性的修改。再利用编写的函数求出从源点到汇点的所有的可达路径,在获得所有可达路径的同时也获取了所有可达路径所花费的时间,那么时间最大的就是关键路径。该方法不仅简便直观,而且能够在保证正确性合理性的前提下提高执行效率,减小时间复杂度。     

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.     

Functional semantics of programs with exceptions

Linguistic mechanisms for exception handling facilitate the production of reliable software and play an important role in fault tolerant computing. This paper describes the functional semantics of a Pascal-like language which supports exception handling and data abstraction. A program with exceptions is considered as having a standard semantics, as well as an exceptional semantics for each exception that may be signaled during its execution. Standard functional semantics methods provide rules to obtain the function representing the standard semantics. In this paper, we provide rules to determine the functions representing the exceptional semantics. We also describe a method for specifying and verifying the correctness of implementation of data types with exceptions.     

Formal foundation of consistent EMF model transformations by algebraic graph transformation

Model transformation is one of the key activities in model-driven software development. An increasingly popular technology to define modeling languages is provided by the Eclipse Modeling Framework (EMF). Several EMF model transformation approaches have been developed, focusing on different transformation aspects. To validate model transformations with respect to functional behavior and correctness, a formal foundation is needed. In this paper, we define consistent EMF model transformations as a restricted class of typed graph transformations using node type inheritance. Containment constraints of EMF model transformations are translated to a special kind of graph transformation rules such that their application leads to consistent transformation results only. Thus, consistent EMF model transformations behave like algebraic graph transformations and the rich theory of algebraic graph transformation can be applied to these EMF model transformations to show functional behavior and correctness. Furthermore, we propose parallel graph transformation as a suitable framework for modeling EMF model transformations with multi-object structures. Rules extended by multi-object structures can specify a flexible number of recurring structures. The actual number of recurring structures is dependent on the application context of such a rule. We illustrate our approach by selected refactorings of simplified statechart models. Finally, we discuss the implementation of our concepts in a tool environment for EMF model transformations.     

Completion of Rewrite Systems with Membership Constraints Part I: Deduction Rules

We consider a constrained equational logic where the constraints are membership conditions t∈swheresis interpreted as a regular tree language. Our logic includes a fragment of second-order equational logic (without projections) where second-order variables range over regular sets of contexts. The problem with constrained equational logics is the failure of the critical pair lemma. This is the reason why we propose new deduction rules for which the critical pair lemma is restored. Computing critical pairs requires, however, solving some constraints in a second-order logic with membership constraints. In a second paper we give a terminating set of transformation rules for these formulas, which decides the existence of a solution, thus showing a new term scheme unification algorithm.Since an order-sorted signature is nothing but a bottom–up tree automaton, order-sorted equational logic falls into the scope of our study; our results show how to perform order-sorted completion without regularity and without sort-decreasingness. It also shows how to perform unification in the order-sorted case, with some higher-order variables (without any regularity assumption).