非线性代数规范的直接实现技术

代数规范是支持软件规格说明和设计的一种有效的方法，代数规范的直接实现技术是该研究领域的一个主要分支，目前这方面的研究基本上局限于线性代数规范，本文介绍一个实现非线性代数规范的转换过程，从该过程可自然是导出针对不同程序设计语言的转换系统，我们已实现了一个基于Ｐａｓｃａｌ语言的转换系统。     

Toward formal development of programs from algebraic specifications: Parameterisation revisited

Parameterisation is an important mechanism for structuring programs and specifications into modular units. The interplay between parameterisation (of programs and of specifications) and specification (of parameterised and of non-parameterised programs) is analysed, exposing important semantic and methodological differences between specifications of parameterised programs and parameterised specifications. The extension of parameterisation mechanisms to the higher-order case is considered, both for parameterised programs and parameterised specifications, and the methodological consequences of such an extension are explored.A specification formalism with parameterisation of an arbitrary order is presented. Its denotational-style semantics is accompanied by an inference system for proving that an object satisfies a specification. The formalism includes the basic specification-building operations of the ASL specification language and is institution independent.     

CASL: the Common Algebraic Specification Language

The Common Algebraic Specification Language (CASL) is an expressive language for the formal specification of functional requirements and modular design of software. It has been designed by COFI, the international Common Framework Initiative for algebraic specification and development. It is based on a critical selection of features that have already been explored in various contexts, including subsorts, partial functions, first-order logic, and structured and architectural specifications. CASL should facilitate interoperability of many existing algebraic prototyping and verification tools.This paper gives an overview of the CASL design. The major issues that had to be resolved in the design process are indicated, and all the main concepts and constructs of CASL are briefly explained and illustrated — the reader is referred to the CASL Language Summary for further details. Some familiarity with the fundamental concepts of algebraic specification would be advantageous.     

On the algebra of structured specifications

We develop module algebra for structured specifications with model oriented denotations. Our work extends the existing theory with specification building operators for non-protecting importation modes and with new algebraic rules (most notably for initial semantics) and upgrades the pushout-style semantics of parameterized modules to capture the (possible) sharing between the body of the parameterized modules and the instances of the parameters. We specify a set of sufficient abstract conditions, smoothly satisfied in the actual situations, and prove the isomorphism between the parallel and the serial instantiation of multiple parameters. Our module algebra development is done at the level of abstract institutions, which means that our results are very general and directly applicable to a wide variety of specification and programming formalisms that are rigorously based upon some logical system.     

Algebraic implementation of abstract data types

Starting with a review of the theory of algebraic specifications in the sense of the ADJ-group a new theory for algebraic implementations of abstract data types is presented.While main concepts of this new theory were given already at several conferences this paper provides the full theory of algebraic implementations developed in Berlin except of complexity considerations which are given in a separate paper. The new concept of algebraic implementations includes implementations for algorithms in specific programming languages and on the other hand it meets also the requirements for stepwise refinement of structured programs and software systems as introduced by Dijkstra and Wirth. On the syntactical level an algebraic implementation corresponds to a system of recursive programs while the semantical level is defined by algebaic constructions, called synthesis, restriction and identification. Moreover the concept allows composition of implementations and a rigorous study of correctness. The main results of the paper are different kinds of correctness criteria which are applied to a number of illustrating examples including the implementation of sets by hash-tables. Algebraic implementations of larger systems like a histogram or a parts system are given in separate case studies which, however, are not included in this paper.     

A Tool Support for Reusing ELAN Rule-Based Components

The adaptation of software components developed for a specific application in order to generate reusable components often includes some kind of generalization. This generalization may be carried out, for instance, by the renaming of some identifiers or by its parameterization. In our work, we are specially interested in the generalization by parameterization of algebraic specification components. Generalization and some other transformations on algebraic specifications are being integrated in the FERUS tool. This tool was initially developed for the Common Algebraic Specification Language, called CASL, and we show in the paper its adaptation to the new version of the rule-based programming language ELAN.     

从BPMN模型导出组合服务的代数规约

针对应用规约自动测试BPEL表示组合服务时需要解决BPEL服务的规约生成问题,提出了一种从BPMN模型导出BPEL规范定义的组合Web服务的由代数规约语言CASOCC-WS表示的代数规约方法。首先,定义从BPMN模型转换成基调的规则和从BPMN结构转换成正则表达式的规则,设计由正则表达式导出构成公理的项的算法;然后,提出根据所得的项人工书写公理的启发式规则;最后,实现一个从BPMN模型导出组合服务基调的工具原型。案例研究表明,该方法可以解决BPEL服务的代数规约生成问题。     

Exhaustive test sets for algebraic specifications

In the context of testing from algebraic specifications, test cases are ground formulas chosen amongst the ground semantic consequences of the specification, according to some possible additional observability conditions. A test set is said to be exhaustive if every programme P passing all the tests is correct and if for every incorrect programme P, there exists a test case on which P fails. Because correctness can be proved by testing on such a test set, it is an appropriate basis for the selection of a test set of practical size. The largest candidate test set is the set of observable consequences of the specification. However, depending on the nature of specifications and programmes, this set is not necessarily exhaustive. In this paper, we study conditions to ensure the exhaustiveness property of this set for several algebraic formalisms (equational, conditional positive, quantifier free and with quantifiers) and several test hypotheses. Copyright © 2016 John Wiley & Sons, Ltd.     

服务组合的代数规约

现有的服务组合描述途径不能有效地验证和测试组合正确性,针对这一问题,提出了一个代数规约方法,引入规约包机制扩展面向服务代数规约语言SOFIA以支持该方法。用代数规约单元描述服务系统中的各种实体,其中基调部分定义实体的语法和结构,公理部分定义其功能和行为特性。与一个服务相关的规约单元封装在一个包中或拆分在几个相互引用的包中,每个包形成一个命名空间。当多个服务组合在一起时,以这些服务的代数规约包为基础,一方面抽象地定义组合服务的交互过程和语义,形成描述服务组合实现方式的实现规约包;另一方面抽象地定义组合服务对外接口及其功能语义,形成描述组合服务需求的抽象规约包。在实现规约和抽象规约的双元结构基础上,进一步定义了实现规约和抽象规约之间必须满足的“实现”关系,证明了满足实现关系可以保证实现的正确性,从而为服务组合的可验证性和可测试性奠定了理论基础。最后结合实例分析阐述了用代数规约描述服务组合的抽象性、可表达性和可验证性。     

An incremental approach to automatic algorithm design

This paper presents an incremental approach to automatic algorithm design,which can be described by algebraic specifications precisely and conveniently.The definitions of selection operator and extension operator which ca be defined by strategy relations and transformations are given in order to model the process of finding the solution of a problem.Also discussed is its object-oriented implementation.The functional specification and the design specification for an algorithm are given in one framework so that the correctness of the algorithm can be easily proved.     

Algebraic and operational semantics of specifications allowing exceptions and errors

The specification of abstract data types requires the possibility to treat exceptions and errors. We present an approach allowing all forms of error handling: error introduction, error propagation and error recovery. The algebraic semantics of our method and a new correctness criterion are given. We also introduce an operational semantics of a subclass of our specifications which coincides with the algebraic semantics.     

一类半正定多项式的平方和分解及其表达式的自动生成

建立了一个把半正定稀疏多项式表为多项式平方和的算法.这一算法依赖于Hilbert第17问题的一系列经典研究结果以及实闭域上量词消去的柱形代数剖分算法.该算法的机器实现为一类代数不等式可读性证明的自动生成提供了一种非常自然的途径.     

On institutions for modular coalgebraic specifications

We present an algebraic extension of standard coalgebraic specification techniques for state-based systems which allows us to integrate constants and n-ary operations in a smooth way and which leads to institutions enabling the use of modular specification techniques. A sound and complete proof system for first-order observational properties of modular specifications is given. The framework of (Ω,Ξ)-structures that we present can be considered as the result of a transformation of concepts of observational logic as in Hennicker and Bidoit (in: A. Haeberer (Ed.), Algebraic Methodology and Software Technology (AMAST’98), Lecture Notes in Computer Science, vol. 1548, Springer, Berlin, 1999) into the coalgebraic world. Moreover, it is shown that the features of (Ω,Ξ)-structures that make them suitable models for an observational approach to specifications can be categorically expressed by the fact that the operation mapping an (Ω,Ξ)-structure to its behaviour is a fibred idempotent monad.     

最优代数免疫布尔函数的完全构造

任意的布尔函数可以唯一地表示成有限域上的单变元多项式函数,利用布尔函数的单变元多项式表示和代数编码理论,讨论了布尔函数的代数免疫达到最优的判别条件,得到了布尔函数的变元个数为奇数时,布尔函数具有最优代数免疫(MAI)的等价判别条件。利用该等价判别条件,给出3元布尔函数满足MAI的等价判别条件,进而构造出所有3元的MAI布尔函数。     

A relational language with deductions,functions and recursions

We propose here a .relational algebra capable of deducing tuples from a premise expressed in an extended relational form: it also supports user-defined and recursive functions in the form of parameterised views, and provides a facility for easier specification of queries. The paper shows the power of the language in dealing with problems such as ancestors, part explosions and connected tours.This language, called DEAL, is an enhanced version of the PRECI Algebraic Language (PAL) but presented here in a SQL-like syntax.     

布尔函数代数免疫度的研究

代数免疫度是度量布尔函数抵抗代数攻击的重要指标。为了抗代数攻击,布尔函数应具有较高的代数免疫度。对于给定的奇数n,得到一个具有最大代数免疫度的布尔函数重量的可除性结果,同时,在任意有限域上,针对关系式fg=h,研究了它的代数免疫度,给出了一些重要结果。     

DFA模型及其语言的结构化代数规约

本文首先阐述了利用ＤＦＡ模型技术进行状态转换系统描述存在的主要问题,提出了利用代数规约技术解决这些问题的可行性,然后介绍了新一代具有松散语义的代数规约语言ＳＰＥＣＴＲＵＭ及其主要规约操作符的语法和语义,并根据ＤＦＡ模型及其语言的数学定义,给出了它们的结构化代数规约,为基于ＤＦＡ模型的状态转换系统的形式化设计和开发奠定了基础。     

具有最大代数免疫度的奇数元布尔函数的构造

构造一个具有最大代数免疫度的奇数元布尔函数等价于在某一已知矩阵中寻找一个可逆子矩阵。如何在这一矩阵中有效地寻找可逆子矩阵仍然是一个难题。针对上述问题研究矩阵的性质,简化矩阵的刻画方式,给出构造最大代数免疫度的奇数元布尔函数的构造方法。构造时只需对低维数的向量进行操作,避免了子矩阵可逆性的判断,能够有效地构造具有最大代数免疫度的奇数元布尔函数。