Equivalence of formal semantics definition methods

There are numerous methods of formally defining the semantics of computer languages. Each method has been designed to fulfil a different purpose. For example, some have been designed to make reasoning about languages as easy as possible; others have been designed to be accessible to a large audience and some have been designed to ease implementation of languages. Given two semantics definitions of a language written using two separate semantics definition methods, we must be able to show that the two are in fact equivalent. If we cannot do this then we either have an error in one of the semantics definitions, or more seriously we have a problem with the semantics definition methods themselves.Three methods of defining the semantics of computer languages have been considered, i.e. Denotational Semantics, Structural Operational Semantics and Action Semantics. An equivalence between these three is shown for a specific example language by first defining its semantics using each of the three definition methods. The proof of the equivalence is then constructed by selecting pairs of the semantics definitions and showing that they define the same language.A full version of this paper can be accessed via our web page http://www.cs.man.ac.uk/fmethods/ facj.html     

Towards a formal definition of methods

The absence of a formal specification of methods permits application engineers to interpret method concepts in any way they want. Further, different CASE tool designers can implement the same method concepts in different ways. The approach to formal method specification described here is in three levels: the generic level, the method independent level, and the method level. The generic level provides a model of a method which can be instantiated to yield a method-independent view of methods. This view can, in turn, be instantiated to yield the formal method of interest. The attempt is to represent methods independently of any underlying way-of-working or paradigm, remove the process/product dichtomy by tight coupling of the process and product aspects of methods, and permit extensibility of methods. The formal specification can be used as a basis for building CASE tools, as an output to be produced by a CAME tool, and for defining development processes.     

Testing restorable systems: formal definition and heuristic solution based on river formation dynamics

Given a finite state machine denoting the specification of a system, finding some short interaction sequences capable of reaching some/all states or transitions of this machine is a typical goal in testing methods. If these sequences are applied to an implementation under test, then equivalent states or transitions would be reached and observed in the implementation—provided that the implementation were actually defined as the specification. We study the problem of finding such sequences in the case where configurations previously traversed can be saved and restored (at some cost). In general, this feature enables sequences to reach the required parts of the machine in less time, because some repetitions can be avoided. However, we show that finding optimal sequences in this case is an NP-hard problem. We propose an heuristic method to approximately solve this problem based on an evolutionary computation approach, in particular river formation dynamics (RFD). Given finite state machine specifications and sets of states/transitions to be reached, we apply RFD to construct testing plans reaching these configurations. Experimental results show that being able to load previously traversed states generally reduces the time needed to cover the target configurations.     

The formal definition of a real-time language

Summary This paper presents the formal definition of TOMAL (Task-Oriented Microprocessor Applications Language), a programming language intended for real-time systems running on small processors. The formal definition addresses all aspects of the language. Because some modes of semantic definition seem particularly well-suited to certain aspects of a language, and not as suitable for others, the formal definition employs several complementary modes of definition.The primary definition is axiomatic and is employed to define most statements of the language. Simple, denotational (but not lattice-theoretic) semantics complement the axiomatic semantics to define type-related features, such as binding of names to types, data type coercions, and evaluation of expressions. Together, the axiomatic and denotational semantics define all features of the sequential language. An operational definition is used to define real-time execution, and to extend the axiomatic definition to account for all aspects of concurrent execution. Semantic constraints, sufficient to guarantee conformity of a program with the axiomatic definition, can be checked by analysis of a TOMAL program at compilation.     

知识定义及转化研究

通过分析已有知识定义和分类,找出知识定义的共性和当前定义存在的不足,以集合形式对知识进行重新定义;剖析知识与数据、信息和智慧之间的关系,给出知识的传播模式,总结基于K-Set定义的知识特性;以K-Set视角对SECI模型进行解读,剖析其作为知识创造模型存在的缺陷。     

The formal definition of semantics by string automata

An abstract machine called a string automaton (SA) is introduced in this paper. SAs are motivated by the need to formally define the semantics of programming languages in a manner accessible to the users of the language. The SA notation can be used to represent functions and computations in a clear, concise, graphical, and natural manner. After the class of SAs has been formally defined, it is shown how logic modules (resembling hardware circuit elements) and function modules (which define functions) can be expressed by SAs. Networks of SAs and their application to the construction of parsers is discussed. The definition of the language and hardware components of an interactive programming system by means of SAs is outlined.     

The formal definition of human/ machine communications

The specification of human/machine dialogues for general purpose terminals and special purpose consoles in a natural language is difficult and frequently leads to ambiguities and misinterpretations between terminal and dialogue constructors and users. In this paper, the problem of operator console definition is related to the problem of language and language translator definition. An efficient metalanguage tool (TBNF) for the handling of the latter problem is applied to the solution of the first problem. An example from the Telecontrol of a Power Network, being developed at ENHER (Barcelona, Spain), is described as an illustration.     

On a formal definition and application of dimensional design

Dimensional design (DD) is a simple, practical and systematic layout technique for the display of programs, specifications, expressions, etc. for application in the general area of software. Formalizations of DD are introduced, the main one being algebraic, and the usage of DD in real software projects is outlined; one of them corresponds to a software system for the telecontrol centre of a power network. The formal definitions of DD which are presented arise during the design of a syntax-driven editor generator for languages whose ‘phrases’ are DDs. Grammars for the definition of such languages are introduced in the paper. The varied usage of DD within the generator design is examined: grammatical, functional and algebraic notations in particular are considered. The samples of these DD representations that are given illustrate the enhancement of readability achieved, and illustrate the suitability of DD for use in the specification area in general.     

A model for the formal definition of programming languages

An operational model which allows the complete formal definition of the full syntax and, particularly, semantics of programming languages is described. Both its syntactic and semantic parts are based on so-called linked-forest manipulation systems which allow the definition of mappings on forests. The idea of “linking” is crucial for the given model, we represent not only abstract programs but also intermediate states of our system (abstract computer) by labelled forests with pointers.     

A formal definition of the Hough transform: Properties and relationships

Shape, in both 2D and 3D, provides a primary cue for object recognition and the Hough transform (P.V.C. Hough, U.S. Patent 3,069,654, 1962) is a heuristic procedure that has received considerable attention as a shape-analysis technique. The literature that covers application of the Hough transform is vast; however, there have been few analyses of its behavior. We believe that one of the reasons for this is the lack of a formal mathematical definition. This paper presents a formal definition of the Hough transform that encompasses a wide variety of algorithms that have been suggested in the literature. It is shown that the Hough transform can be represented as the integral of a function that represents the data points with respect to a kernel function that is definedimplicitly through the selection of a shape parameterization and a parameter-space quantization. The kernel function has dual interpretations as a template in the feature space and as a point-spread function in the parameter space. A novel and powerful result that defines the relationship between parameterspace quantization and template shapes is provided. A number of interesting implications of the formal definition are discussed. It is shown that the Radon transform is an incomplete formalism for the Hough transform. We also illustrate that the Hough transform has the general form of a generalized maximum-likelihood estimator, although the kernel functions used in estimators tend to be smoother. These observations suggest novel ways of implementing Hough-like algorithms, and the formal definition forms the basis of work for optimizing aspects of Hough transform performance (see J. Princen et. al.,Proc. IEEE 3rd Internat. Conf. Comput. Vis., 1990, pp. 427–435).This work was supported by the Ministry of Defence, Royal Aerospace Establishment, U.K.     

基于形式化规格说明的UML状态图提取

为了辅助软件开发者理解形式化规格说明,提出一种从B方法规格说明中提取UML状态图的方法。通过分析状态信息在规格说明中的表现形式,定义一系列精确的简单状态、状态迁移、复合迁移、分层状态和状态图通信等提取规则。借助状态变量表和状态迁移表,最终实现状态元素和状态关系的提取,并以此构造完整的UML状态图。实验结果验证了方法的正确性及有效性。     

基于形式化描述测试用例生成的研究与实现

根据高安全系统实现和评估的需要,提出基于形式化Z描述的测试用例生成方法,并据此实现了测试用例自动生成工具,可进行符合更改条件/判定覆盖准则的测试用例生成,以解决生成测试用例数量与质量间的取舍问题。与相关工作相比,可以降低形式化描述的要求,减少人工参与的成分,提高测试用例生成的有效性和效率。     

基于形式化方法的测试驱动开发研究

对测试驱动开发中测试用例的自动生成和管理问题进行了研究,并时现有方法进行了分析和比较.给出了一种基于形式化方法的测试用例生成和管理方案.该方案通过形式化语言描述软件规约,并通过相应工具生成和管理测试用例,从而提高了测试驱动开发的效率.最后给出了该方案在极限编程各个开发阶段的应用.     

Reliable yet flexible software through formal model transformation (rule definition)

The results of literature review show that the need for both reliability and flexibility is increasingly becoming important among the various classes of software applications. Developing reliable yet flexible software is a hard problem. Although modeling methods enjoy a lot of advantages, the use of just one of them, in many cases, may not guarantee the development of reliable and flexible software. Formal modeling methods ensure reliability. However, lack of knowledge and high cost practically force developers to use semi-formal methods instead. Semi-formal (visual) modeling methods, which are widely used in practical large-scale software development, are not good enough for reliable software development. This paper proposes a new practical approach to the development of reliable yet flexible software. In the proposed approach, formal (Object-Z) and semi-formal (UML) models are transformed into each other using a set of bidirectional formal rules. Formal modeling and refinement ensure the reliability of software. Visual models facilitate the interactions among stakeholders who are not familiar enough with the complex mathematical concepts of formal methods. Visual models help detect the unexpected behavior and inconsistencies of software. Applying design patterns to visual models improves the flexibility of software. The transformation of formal and visual models into each other through the iterative and evolutionary process, proposed in this paper, helps develop the software applications that need to be highly reliable yet flexible. The feasibility of the proposed approach is evaluated using the multi-lift case study.     

Parameter reference immutability: formal definition, inference tool, and comparison

Knowing which method parameters may be mutated during a method’s execution is useful for many software engineering tasks. A parameter reference is immutable if it cannot be used to modify the state of its referent object during the method’s execution. We formally define this notion, in a core object-oriented language. Having the formal definition enables determining correctness and accuracy of tools approximating this definition and unbiased comparison of analyses and tools that approximate similar definitions. We present Pidasa, a tool for classifying parameter reference immutability. Pidasa combines several lightweight, scalable analyses in stages, with each stage refining the overall result. The resulting analysis is scalable and combines the strengths of its component analyses. As one of the component analyses, we present a novel dynamic mutability analysis and show how its results can be improved by random input generation. Experimental results on programs of up to 185 kLOC show that, compared to previous approaches, Pidasa increases both run-time performance and overall accuracy of immutability inference.     

Macro and File Structure Preservation in Source-to-source Translation

This paper describes a strategy for translating macro definitions and uses in the context of performing automated source-to-source translation between high-level programming languages. This translation technology enables macros and other preprocessor structures to be preserved in the generated source. It is useful for generating readable and maintainable code.     

Prototyping realistic programming languages based on formal specifications

The specification of realistic programming languages is difficult and expensive. One approach to make language specification more attractive is the development of techniques and systems for the generation of language–specific software from specifications. To contribute to this approach, a tool–based framework with the following features is presented: It supports new techniques to specify more language aspects in a static fashion. This improves the efficiency of generated software. It provides powerful interfaces to generated software components. This facilitates the use of these components as parts of language–specific software. It has a rather simple formal semantics. In the framework, static semantics is defined by a very general attribution technique enabling e.g. the specification of flow graphs. The dynamic semantics is defined by evolving algebra rules, a technique that has been successfully applied to realistic programming languages. After providing the formal background of the framework, an object–oriented programming language is specified to illustrate the central specification features. In particular, it is shown how parallelism can be handled. The relationship to attribute grammar extensions is discussed using a non-trivial compiler problem. Finally, the paper describes new techniques for implementing the framework and reports on experiences made so far with the implemented system. Received: 20 November 1995 / 20 January 1997     

基于UML的形式化规范说明研究

软件的规范说明阶段 ( specification phase)对于软件的整体开发过程来说是一个非常重要的阶段 ,UML方法是目前比较流行的软件工程开发方法 ,它对软件整体开发过程提供了一套有用的模型。本文根据 UML和谓词转换 ,提出一种面向对象的形式化规范说明方法 ,并给出一组和 UML相对应的数学模型。本文的方法吸收了 UML和一般形式化方法的优点 ,具有数学的严谨性和精确性 ,并且更加易于理解和表达。     

基于形式概念分析的粗糙描述逻辑研究

以往的粗糙描述逻辑(RDL)都是基于传统的粗糙集理论。实际上,经常会出现用形式概念表示一个概念的情况,此时一个自然的问题就是如何处理可能出现的不确定概念。把形式概念分析与粗糙集理论联系起来做为基础,给出可定义概念和不可定义概念的定义,并给出不可定义概念的上近似和下近似,这里的近似定义虽然不同于传统的粗糙近似算子形式,但是有很好的实用性。基于新的上下近似定义,把一组近似算子引入到描述逻辑的结构中,形成一种新的粗糙描述逻辑。给出了相应的语法和语义,最后还给出了扩展的Tableau算法,可以用来解决相应的推理问题。