面向对象的契约式程序设计

运用行为子类型及扩充行为子类型的概念，通过对一个Java实例地剖析，讨论了在面向对象的契约式程序设计中如何撰写契约，以保持面向对象的单个继承和多重继承的特性问题，并证明了这一方法的有效性。最后探讨了动态环境下违反契约时的责任归咎，展望了契约思想在软件开发中的运用前景。     

契约式设计在可信业务构件中的应用

介绍了契约式设计的思想，并在业务构件的分析中引入了契约式设计，从而构造出可信的业务构件。重点分析了契约式设计如何通过前置条件、后置条件和不变式3要素保证业务构件的可信，并给出具体的实例来说明。     

Executing Formal Specifications with Concurrent Constraint Programming

We have implemented a technique for execution of formal, model-based specifications. The specifications we can execute are written at a level of abstraction that is close to that used in nonexecutable specifications. The specification abstractions supported by our execution technique include using quantified assertions to directly construct post-state values, and indirect definitions of post-state values (definitions that do not use equality). Our approach is based on translating specifications to the concurrent constraint programming language AKL. While there are, of course, expressible assertions that are not executable, our technique is amenable to any formal specification language based on a finite number of intrinsic types and pre- and postcondition assertions.     

基于c#的合约式包装器的设计方案研究

实现了一个C#语言的合约检查工具,用于辅助程序员在用C#语言编写软件的时候运用合约式设计方法。工具将书写在程序注释中的合约提取出来,并转化为类不变式、类方法的前置条件或后置条件的检查代码插入到源文件中。当执行含有合约检查代码的源文件的时候,检查代码将被执行,以确保合约是否被遵守。     

Interface theories for concurrency and data

We present a compositional approach for specifying concurrent behavior of components with data states on the basis of interface theories. The dynamic aspects of a system are specified by modal input/output automata, whereas changing data states are specified by pre- and postconditions. The combination of the two formalisms leads to our notion of modal input/output automata with data constraints (MIODs). In this setting we study refinement and behavioral compatibility of MIODs. We show that compatibility is preserved by refinement and that refinement is compositional w.r.t. synchronous composition, thus satisfying basic requirements of an interface theory. We propose a semantic foundation of interface specifications where any MIOD is equipped with a model-theoretic semantics describing the class of its correct implementation models. Implementation models are formalized in terms of guarded input/output transition systems and the correctness notion is based on a simulation relation between an MIOD and an implementation model which relates not only abstract and concrete control states but also (abstract) data constraints and concrete data states. We show that our approach is compositional in the sense that locally correct implementation models of compatible MIODs compose to globally correct implementations, thus ensuring independent implementability.     

Validating UML and OCL models in USE by automatic snapshot generation

We study the testing and certification of UML and OCL models as supported by the validation tool USE. We extend the available USE features by introducing a language for defining properties of desired snapshots and by showing how such snapshots are generated. Within the approach, it is possible to treat test cases and validation cases. Test cases show that snapshots having desired properties can be constructed. Validation cases show that given properties are consequences of the original UML and OCL model.     

Two theorems about the completeness of Hoare's logic

We prove two theorems about the completeness of Hoare's logic for the partial correctness of while-programs over an axiomatic specification. The first result is a completion theorem: any specification (Σ,E) can be refined to a specification (Σ₀, E₀), conservative over (Σ, E), whose Hoare's logic is complete. The second result is a normal form theorem: any complete specification (Σ, E) possessing some complete logic for partial correctness can be refined to an effective specification (Σ₀, E₀) conservative over (Σ, E), which generates all true partial correctness formulae with Hoare's standard rules.