智能对象语言CLOS的分布实现

ＣＬＯＳ系统是一个嵌入Ｃｏｍｍｏｎ Ｌｉｓｐ的面向对象标准语言。文中结合所提出的类分方法，通过引入同步或异步通信协议和ＲＰＣ并发控制，详细介绍了一个新的分布ＣＬＯＳ系统ＰａｒＣＬＯＳ。     

CLOS的分布实现技术

ＣＬＯＳ系统是一个嵌入ＣｏｍｍｏｎＬｉｓｐ的面向对象标准语言，本文结合我们提出的类划分方法，通过引入同步或异步通信协议和ＲＰＣ并发控制，详细介绍了一个新的分布ＣＬＯＳ系统ＰａｒＣＬＯＳ。测试结果表明：若结点较均匀，运行效率大于８０％。     

Visual Lisp/CLOS programming in OpenMusic

OpenMusic (OM) is a visual programming language developed on top of Common Lisp and CLOS, in which most of the functional and object-oriented programming concepts can be implemented and carried out graphically. Although this visual language was designed for musical applications, the focus in this paper is to describe and study OM as a complete general-purpose programming environment.     

Designing a browser to support multimethods and method combination

This paper describes some of the design considerations in developing a tool for maintaining generic functions in the proposed Common Lisp Object-Oriented System (CLOS). It is argued that tools based on class lattices provide insufficient support for programming in a language that utilizes multimethods and method combination. A new type of browser, known as a Generic Function Browser (GFB), was designed to handle the more complicated style of procedure definition offered in CLOS. Some simple example of the use of this tool are provided, along with a discussion of the philosophy underlying its design.The work described here was initially undertaken while the author was employed at Xerox AI Systems.     

A verified Common Lisp implementation of Buchberger’s algorithm in ACL2

In this article, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort.     

An environment for DEVS-based multiformalism simulation in Common Lisp/CLOS

The paper presents the realization of an object-oriented kernel of a new modeling and simulation environment. The kernel system stands out as it is based on systems theoretical concepts and facilitates combined discrete-continuous, modular, hierarchical modeling. Its implementation language is the AI language Common Lisp and its object-oriented superset CLOS. The kernel system serves as the basis for a knowledge-based modeling and simulation environment supporting interactive modeling and simulation and automatic model construction. This research was supported in part by SIEMENS Munich, ZFE, ST.     

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

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

一个基于广义函数机制的反射结构

本文讨论了一个以扩充Ｌｉｓｐ方式实现的ＣＬＯＳ系统中的反射结构及其实现技术，该反射结构基于统一的对象表示，支持广义化对象模型，与宿主语言的反射有一致性．其中的反射计算采用了ＣＬＯＳ的元对象协议的思想．     

HasCasl: Integrated higher-order specification and program development

We lay out the design of HasCasl, a higher order extension of the algebraic specification language Casl that serves both as a wide-spectrum language for the rigorous specification and development of software, in particular but not exclusively in modern functional programming languages, and as an expressive standard language for higher-order logic. Distinctive features of HasCasl include partial higher order functions, higher order subtyping, shallow polymorphism, and an extensive type-class mechanism. Moreover, HasCasl provides dedicated specification support for monad-based functional-imperative programming with generic side effects, including a monad-based generic Hoare logic.     

Endpaper: Technical issues of separation in function cells and value cells

Summary The bulk of arguments that focus on clean semantics and notational simplicity tend to favor uniting the function and value namespaces. In spite of this, there are those who hold strongly to a belief that a two-namespace system affords useful expressive power that they are unwilling to do without. In the end, practical considerations favor the status quo for Common Lisp. There are a large number of improvements beyond a single namespace that could be made to Common Lisp that would clean it up and simplify it. We feel that the time for such radical changes to Common Lisp has passed, and it is the job of future Lisp designers to take the lessons from Common Lisp and Scheme to produce an improved Lisp.This paper is an adaptation of a report produced for X3J13 by the authors, a technical working group engaged in standardizing Common Lisp for ANSI.     

Coinduction for preordered algebra

We develop a combination, called hidden preordered algebra, between preordered algebra, which is an algebraic framework supporting specification and reasoning about transitions, and hidden algebra, which is the algebraic framework for behavioural specification. This combination arises naturally within the heterogeneous framework of the modern formal specification language CafeOBJ. The novel specification concept arising from this combination, and which constitutes its single unique feature, is that of behavioural transition. We extend the coinduction proof method for behavioural equivalence to coinduction for proving behavioural transitions.     

Overview: The common lisp object system

The Common Lisp Object System is an object-oriented system that is based on the concepts of generic functions, multiple inheritance, and method combination. All objects in the Object System are instances of classes that form an extension to the Common Lisp type system. The Common Lisp Object System is based on a meta-object protocol that renders it possible to alter the fundamental structure of the Object System itself.     

Fortran to Lisp Translation using f2cl

The need for both algebraic and numerical capabilities within mathematical computation systems has highlighted the need to translate numerical software written in Fortran77 to Common Lisp, a language favoured by the algebraic computation community. This paper reports the current state of f2cl, a translator written to achieve that end. We describe the translation process giving details of Lisp equivalents of Fortran expressions, as well as discussing features of Fortran that have no straightforward equivalent in Lisp.     

GKS in an object-oriented environment

Because of its basis properties, object-oriented programming is well suited to creating user interfaces or graphical applications. However, object-oriented systems are often without graphics or have only a graphical kernel which presents a very low level of use. Besides, such graphical kernels are dependent on the implementation. The use of graphical standards could be an alternative way to bring portability of the applications. Object-oriented systems are often implemented on top of Common Lisp or similar Lisp dialects. In this paper the implementation of an object-oriented shell of an available GKS implementation using an object-oriented extension of Common Lisp will be discussed.     

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.     

SLAN-4?A Software Specification and Design Language

SLAN-4 (``Software Language-4') was developed to meet the need for a formal tool for specifying and designing large software systems. It provides language constructs for algebraic and axiomatic specifications and also pseudocode constructs for the design step. A major design goal was to ease subsequent refinements of a (given) specification. The design can start with a very informal specification, which can be implemented later using lower level concepts. This paper gives an overview of the SLAN-4 syntax and semantics. It concentrates on the most important aspects of: ? abstract data types, ? algebraic specification of abstract data types, and ? axiomatic specification of modules. Because the pseudocode part of SLAN-4 consists mainly of control structures similar to those in modern high-level programming languages, this element of the language is not separately described. The paper includes an example of how to use SLAN-4, and also the experiences gained in using the language to formally specify a real-world software product of about 18 000 lines of code written in an IBM internal high-level language.     

Detection of metamorphic and virtualization-based malware using algebraic specification

We present an overview of the latest developments in the detection of metamorphic and virtualization-based malware using an algebraic specification of the Intel 64 assembly programming language. After giving an overview of related work, we describe the development of a specification of a subset of the Intel 64 instruction set in Maude, an advanced formal algebraic specification tool. We develop the technique of metamorphic malware detection based on equivalence-in-context so that it is applicable to imperative programming languages in general, and we give two detailed examples of how this might be used in a practical setting to detect metamorphic malware. We discuss the application of these techniques within anti-virus software, and give a proof-of-concept system for defeating detection counter-measures used by virtualization-based malware, which is based on our Maude specification of Intel 64. Finally, we compare formal and informal approaches to malware detection, and give some directions for future research.     

Towards formal open standards: formalizing a standard’s requirements

Open standardization seems to be very popular among software developers as it simplifies the standard’s adoption by the software engineering. Formal specification methods, while very promising, are being adopted slowly as the industry seems to have little motivation to move into this territory. In this paper the authors present (1) the idea of applying formal specification techniques to open standards’ specifications, and (2) an example of a formal specification of the Rich Site Summary (RSS) v2.0 open standard. The authors provide evidence for the advantages of the open standards formal specification over natural language documentations: formal specifications are more concise, less ambiguous, more complete with respect to the original documentation and, when using certain kinds of specification languages, executable and reusable as they support module inheritance. The merging of formal specification methods and open standards allows (1) a more concrete standard design; (2) an improved understanding of the environment under design; (3) an enforced certain level of precision into the specification, and also (4) provides software engineers with extended property checking/verification capabilities, especially if they opt to use any algebraic specification language. The authors showcase how the RSS standard can be formally specified using an algebraic specification language and demonstrate how can that be beneficial.