Effective homology of bicomplexes, formalized in Coq

In this paper, we present a complete formalization in the Coq theorem prover of an important algorithm in computational algebra, namely the calculation of the effective homology of a bicomplex. As a necessary tool, we encode a hierarchy of algebraic structures in constructive type theory, including graded and infinite data structures. The experience shows how some limitations of the Coq proof assistant to deal with this kind of algebraic data can be overcome by applying a separation of concerns principle; more concretely, we propose to distinguish in the representation of an algebraic structure (such as a group or a module) a behavioural part, containing operation signatures and axioms, and a structural part determining if the algebraic data is free, of finite type and so on.     

The RAISE language,method and tools

This paper presents the RAISE¹ software development method, its associated specification language, and the tools supporting it. The RAISE method enables the stepwise development of both sequential and concurrent software from abstract specification through design to implementation. All stages of RAISE software development are expressed in the wide-spectrum RAISE specification language. The RAISE tools form an integrated tool environment supporting both language and method.The paper surveys RAISE and furthermore, more detailed presentations of major RAISE results are provided. The subjects of these are (a) an example of the use of the RAISE method and language, and (b) a presentation of the mathematical semantics of the RAISE specification language.     

Vibes: A visual language for specifying behavioral requirements of algorithms

Manually verifying the behavior of software systems with respect to a set of requirements is a time-consuming and error-prone task. If the verification is automatically performed by a model checker however, time can be saved, and errors can be prevented. To be able to use a model checker, requirements need to be specified using a formal language. Although temporal logic languages are frequently used for this purpose, they are neither commonly considered to have sufficient usability, nor always naturally suited for specifying behavioral requirements of algorithms. Such requirements can be naturally specified as regular language recognizers such as deterministic finite accepters, which however suffer from poor evolvability: the necessity to re-compute the recognizer whenever the alphabet of the underlying model changes. In this paper, we present the visual language Vibes that both is naturally suited for specifying behavioral requirements of algorithms, and enables the creation of highly evolvable specifications. Based on our observations from controlled experiments with 23 professional software engineers and 21 M.Sc. computer science students, we evaluate the usability of Vibes in terms of its understandability, learnability, and operability. This evaluation suggests that Vibes is an easy-to-use language.     

Using the programming walkthrough to aid in programming language design

The programming walkthrough is a method for assessing how easy or hard it will be for users to write programs in a programming language. It is intended to enable language designers to identify problems early in design and to help them choose among alternative designs. We describe the method and present experience in applying it in four language design projects. Results indicate that the method is a useful supplement to existing design approaches.     

A mechanical verification of the stressing algorithm for negative cost cycle detection in networks

The negative cost cycle detection (NCCD) problem in weighted directed graphs is a fundamental problems in theoretical computer science with applications in a wide range of domains ranging from maximum flows to image segmentation. From the perspective of program verification, this problem is identical to the problem of checking the satisfiability of a conjunction of difference constraints. There exist a number of approaches in the literature for NCCD with each approach having its own set of advantages. Recently, a greedy, space-efficient algorithm called the stressing algorithm was proposed for this problem. In this paper, we present a novel proof of the Stressing algorithm and its verification using the Prototype Verification System (PVS) theorem prover. This example is part of a larger research program to verify the soundness and completeness of a core set of decision procedures.     

Steps towards a method for the formal modeling of dynamic objects

Fragments of a method to formally specify object-oriented models of a universe of discourse are presented. The task of finding such models is divided into three subtasks, object classification, event specification, and the specification of the life cycle of an object. Each of these subtasks is further subdivided, and for each of the subtasks heuristics are given that can aid the analyst in deciding how to represent a particular aspect of the real world. The main sources of inspiration are Jackson System Development, algebraic specification of data- and object types, and algebraic specification of processes.     

The RISC ProofNavigator: a proving assistant for program verification in the classroom

This paper gives an overview of the RISC ProofNavigator, an interactive proving assistant for the area of program verification. The assistant combines the user-guided top-down decomposition of proofs with the automatic simplification and closing of proof states by an external satisfiability solver. The software exhibits a modern graphical user interface which has been developed with a focus on simplicity in order to make the software suitable for educational scenarios. Nevertheless, some use cases of a certain level of complexity demonstrate that it may be also appropriate for various realistic applications. D. A. Duce, J. Oliveira, P. Boca and R. Boute     

Towards a language for concurrent processes

In this paper we shall discuss concurrency in programming languages, with a view towards designing a process-oriented language which, by its inherent parallelism, is well suited to exploit the forthcoming generation of distributed processor networks. We shall start by discussing the traditional approach towards managing concurrency, with ‘monitors’ co-ordinating the interactions of ‘processes’, and shall demonstrate that this approach actually degrades concurrency by imposing sequentiality during interactions because it is based on the premise of co-ordinating secure access to shared resources. As a tool for interprocess communication it is felt that the ‘monitor’ is too far removed from the abstract nature of the problem, and so, as a purely engineering solution, it imposes too broad and too prolonged an exclusion to be acceptable in general. Instead we turn to a simpler, and ultimately more powerful notion of ‘message passing’ between parallel processes. We shall show how, if the message system is polymorphic, any data value, however large it is, can pass freely between any pair of processes. By making the processes themselves values in the language we shall discover that message networks can come into being dynamically, and tailor themselves to their applications as and when necessary by ‘short-circuiting’ extensive communications paths. We shall also see how, if the message system is inherently asynchronous, the degree of the parallelism in a system can be enhanced, not degraded, as more and elaborate communications paths develop, the only sequentiality in the system as a whole being imposed by synchronizing processes, not the message passing system itself. After discussing the various built-in system facilities that permit processes to dynamically find out about and study one another, thus permitting processes to set up and thereafter supervise whole subsystems, we shall round off by discussing the advantages of introducing the machines themselves into the language, making it possible for processes to become aware of, and then ‘migrate’ within, the topological structure of a multi-processor distributed network, moving closer to their application, or just to a less-loaded processor, as the need arises. To conclude we shall contrast this new-style process-oriented language with various existing programming languages which have experimented with concurrency, either implicitly or explicitly, in order to see if, and if so how, this new style is any simpler and more powerful than its precursors.     

Mark, a Reasoning Kit for Mobility

The experience gained to date in the development of network applications has shown the difficulties of using traditional software technologies: reasoning about network applications is subtly different from reasoning about ordinary programs because of stronger requirements on security, different forms of termination, and phenomena like mobility and network-awareness. There are currently no standard methods, techniques and tools to support specification, development and (property) certification of these applications.To support property certification of network applications, we propose to use the network-aware logic Mobadtl and its proof assistant, Mark (Mobadtl Reasoning Kit). In the paper we present the prototype implementation of Mark and, as a validating example, we consider applications where mobile components are allowed to carry some resources with them when moving around the network.     

安全协议认证的形式化方法研究

安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向。     

The consistency theorem for free type definitions in Z

Successive editions of the author's reference manual for the Z specification language [ZRM89, ZRM92] gave different sufficient conditions for the consistency of free type definitions. Both were expressed in terms of the settheoretic constructions present in the type definition. Whilst the first edition specified that these constructions should becontinuous, in the sense that they preserve limits of ascending chains of sets, the second edition specified that they should befinitary, i.e., that the result of each construction should be the union of a set of finite approximations. This short note clarifies the relationship between these two conditions.     

Meaningful web annotations for humans and machines using controlled natural language

Abstract: In this paper we present a novel approach that allows humans to create meaningful web annotations in controlled natural language. The controlled natural language serves as a high-level interface language which enables human annotators to summarize individual web pages of a website and to express domain-specific ontological knowledge about that website in an unambiguous subset of English. The annotation process is backed up by an intelligent text editor which supports the writing process of the controlled natural language with the help of predictive interface techniques. The text editor runs as a Java applet and is connected over the Internet to a controlled natural language processor and to a reasoning service (consisting of a theorem prover and a model builder). The controlled language processor translates the summaries of web pages and the ontological knowledge about a website into first-order predicate logic and the reasoning service combines this information into a set of micro-theories for consistency and informativity checking as well as for question-answering. Specification texts written in controlled natural language are both human-readable and machine-processable and can be easily exported and distributed as web feeds.     

UCB策略在Prolog中的应用

Prolog(Programming in Logic)程序语言是一种逻辑程序设计语言.它是在逻辑学理论基础上建立起来的并广泛应用在人工智能研究中.这几十年已经出现了各具特色的Prolog编译器,而且各种编译器也都很成功.虽然在现阶段已经出现了各种版本Prolog编译器,但是Prolog编译器的发展空间还是很大.本文先通过现代Prolog编译器的不足,介绍了新Prolog编译器的特点,然后简单叙述了Prolog编译器词法分析和语法分析的过程,最后介绍了UCB策略.     

The development of a specification language for a computer security system

The primary goal of this paper is to define an initial step towards the definition of ‘systems grammar’ based on the notion of formal languages which can be used as a ‘tool’ in the formal representation of computer security systems. Currently all modelling done on computer security systems is written up as mathematical models. These mathematical models are usually based on the mathematics of relations amongst objects, as opposed to the model described in this paper which is based on the theory of formal languages. This paper is aimed at people who are doing research on the logical aspects of computer security. It is the first of a series of two papers. This paper will give interim results and make more specific the definition of a ‘formal language’ which suits the computer security environment. The second paper will illustrate the actual use of the defined ‘formal language’ and show how to represent the characteristics of a computer security environment by using this ‘formal language’.     

VSE: formal methods meet industrial needs

The Verification Support Environment (VSE) is a tool to formally specify and verify complex systems. It provides the means to structure specifications and supports the development process from the specification of a system to the automatic generation of code. Formal developments following the VSE method are stored and maintained in an administration system that guides the user and maintains a consistent state of development. An integrated deduction system provides proof support for the deduction problems arising during the development process. We describe the application of VSE to an industrial case study and give an overview of the enhanced VSE system and the VSE methodology.     

Using units of measurement in formal specifications

In the physical sciences and engineering, units of measurement provide a valuable aid to both the exposition and comprehension of physical systems. In addition, they provide an error checking facility comparable to static type checking commonly found with programming languages. It is argued that units of measurement can provide similar benefits in the specification and design of software and computer systems.To demonstrate this, we present an extension of the Z specification notation with support for the incorporation of units in specifications and demonstrate the feasibility of static dimensional analysis of the resulting language.