77 (1-2) 2007

1. Preface i-iv
2. Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B
   Jean-Raymond Abrial,  Stefan Hallerstede 1-28
   We argue that formal modeling should be the starting point for any serious development of computer systems. This claim poses a challenge for modeling: at first it must cope with the constraints and scale of serious developments. Only then it is a suitable starting point. We present three techniques, refinement, decomposition, and instantiation, that we consider indispensable for modeling large and complex systems. The vehicle of our presentation is Event-B, but the techniques themselves do not depend on it.
3. Retrenching the Purse: The Balance Enquiry Quandary, and Generalised and (1, 1) Forward Refinements
   Richard Banach,  Czeslaw Jeske, Michael Poppleton,  Susan Stepney 29-69
   Some of the success stories of model based refinement are recalled, as well as some of the annoyances that arise when refinement is deployed in the engineering of large systems. The way that retrenchment attempts to alleviate such inconveniences is briefly reviewed. The Mondex Electronic Purse formal development provides a highly credible testbed for examining how real world refinement difficulties can be treated via retrenchment. The contributions of retrenchment to integrating the real implementation with the formal development are surveyed, and the extraction of commonly occurring `retrenchment patterns' is recalled. One of the Mondex difficulties, the `Balance Enquiry Quandary' is treated in detail, and the way that retrenchment is able to account for the system behaviour is explained. The problem is reconsidered using generalised forward refinement, and the simplicity of the resolution of the quandary, both by retrenchment, and by generalised forward refinement, inspires the creation of a genuine (1,1) forward refinement for Mondex, something long thought impossible. The forward treatment exhibits a similar balance enquiry quandary to the backward refinement, as it must, given that both are refinements of an atomic action to a non-atomic protocol, and the forward quandary is dealt with as easily by retrenchment as is the backward case. The simplicity of the retrenchment treatment foreshadows a general purpose retrenchment Atomicity Pattern for dealing with atomic-versus-finegrained situations.
4. CoreASM: An Extensible ASM Execution Engine
   Roozbeh Farahbod,  Vincenzo Gervasi,  Uwe Glässer 71-103
   In this paper we introduce a new research effort in making abstract state machines (ASMs) executable. The aim is to specify and implement an execution engine for a language that is as close as possible to the mathematical definition of pure ASMs. The paper presents the general architecture of the engine, together with a high-level description of the extensibility mechanisms that are used by the engine to accommodate arbitrary backgrounds, scheduling policies, and new rule forms.
5. Model Checking Abstract State Machines with Answer Set Programming
   Calvin Kai Fan Tang, Eugenia Ternovska 105-141
   The quality of a computer system can be enhanced by modelling its design and verifying the correctness of the design before implementation is done. Abstract State Machines (ASMs) provide a mathematical framework for system modelling, while Model Checking is a technology for verification of system properties. Together, they form a powerful tool for checking systems. Bounded Model Checking (BMC) based on Answer Set Programming (ASP) is a competitive model checking approach due to its ability to compactly encode BMC problems. In this paper, we present a method of applying ASP to BMC of ASMs. Given an ASM and a temporal property, we show how to efficiently translate the BMC problem for the ASM into a problem of answer set computation. Experimental results for our method using the answer set solvers SMODELS and CMODELS are also given.
6. Time in State Machines
   Susanne Graf, Andreas Prinz 143-174
   State machines are a very general means to express computations in an implementation-independent way. There are ways to extend the abstract state machine (ASM) framework with distribution aspects, but there is no unifying framework for handling time so far.
   We propose event structures extended with time as a natural framework for representing state machines and their true concurrency model at a semantic level and for discussing associated time models. Constraints on these timed event structures and their traces (runs) are then used for characterising different frameworks for timed computations. This characterisation of timed frameworks is independent of ASM and allows to compare time models of different modelling formalisms.
   Finally, we propose some specific extensions of ASM for the expressions of time constraints in accordance with the event-based semantic framework and show the applicability of the obtained framework on an example with a standard time model and a set of consistency properties for timed computations.
7. RAM Simulation of BGS Model of Abstract-state Machines
   Comandur Seshadhri,  Anil Seth,  Somenath Biswas 175-185
   We show in this paper that the BGS model of abstract state machines can be simulated by random access machines with at most a polynomial time overhead. This result is already stated in [5] with a very brief proof sketch. The present paper gives a detailed proof of the result. We represent hereditarily finite sets, which are the typical BGS ASM objects, by membership graphs of the transitive closure of the sets. Testing for equality between BGS objects can be done in linear time in our representation.

77 (3) 2007

1. An Axiomatization of the Token Game Based on Petri Algebras
   Eric Badouel,  Jules Chenou, Goulven Guillou 187-215
   The firing rule of Petri nets relies on a residuation operation for the commutative monoid of non negative integers. We identify a class of residuated commutative monoids, called Petri algebras, for which one can mimic the token game of Petri nets to define the behaviour of generalized Petri nets whose flow relations and place contents are valued in such algebraic structures. The sum and its associated residuation capture respectively how resources within places are produced and consumed through the firing of a transition. We show that Petri algebras coincide with the positive cones of lattice-ordered commutative groups and constitute the subvariety of the (duals of) residuated lattices generated by the commutative monoid of non negative integers. We however exhibit a Petri algebra whose corresponding class of nets is strictly more expressive than the class of Petri nets. More precisely, we introduce a class of nets, termed lexicographic Petri nets, that are associated with the positive cones of the lexicographic powers of the additive group of real numbers. This class of nets is universal in the sense that any net associated with some Petri algebra can be simulated by a lexicographic Petri net. All the classical decidable properties of Petri nets however (termination, covering, boundedness, structural boundedness, accessibility, deadlock, liveness ...) are undecidable on the class of lexicographic Petri nets. Finally we turn our attention to bounded nets associated with Petri algebras and show that their dynamics can be reformulated in term of MV-algebras.
2. A Novel Image Hiding Scheme Based on VQ and Hamming Distance
   Chin-Chen Chang, Wei-Liang Tai, Chia-Chen Lin 217-228
   Data hiding is popularly employed in protecting the copyright, secret information and communication secretly with the convenience of network communication. In order to reduce the amount the transmitted data via network, VQ (vector quantization) is applied to compressing the transmitted data. Since VQ is a low-bit-rate compression scheme, it is difficult to find large redundant hiding space and to get stego-images with high quality for hiding data in VQ-based compressed images. A hiding method for VQ-based compressed images is proposed in this paper according to the Hamming distance between the index values of codewords. Our method makes hiding data more effective and provides stego-images with higher quality than other conventional methods. Experimental results demonstrate the effectiveness and the feasibility of our method.
3. Adaptive Ant Colony Optimization Algorithm Based on Information Entropy: Foundation and Application
   Yancang Li and Wanqing Li 229-242
   In order to solve the premature convergence problem of the basic Ant Colony Optimization algorithm, a promising modification based on the information entropy is proposed. The main idea is to evaluate stability of the current space of represented solutions using information entropy, which is then applied to turning of the algorithm's parameters. The path selection and evolutional strategy are controlled by the information entropy self-adaptively. Simulation study and performance comparison with other Ant Colony Optimization algorithms and other meta-heuristics on Traveling Salesman Problem show that the improved algorithm, with high efficiency and robustness, appears self -adaptive and can converge at the global optimum with a high probability. The work proposes a more general approach to evolutionary-adaptive algorithms related to the population's entropy and has significance in theory and practice for solving the combinatorial optimization problems.
4. Feature Extraction for Dynamic Integration of Classifiers
   Mykola Pechenizkiy, Alexey Tsymbal,  Seppo Puuronen,  David Patterson 243-275
   Recent research has shown the integration of multiple classifiers to be one of the most important directions in machine learning and data mining. In this paper, we present an algorithm for the dynamic integration of classifiers in the space of extracted features (FEDIC). It is based on the technique of dynamic integration, in which local accuracy estimates are calculated for each base classifier of an ensemble, in the neighborhood of a new instance to be processed. Generally, the whole space of original features is used to find the neighborhood of a new instance for local accuracy estimates in dynamic integration. However, when dynamic integration takes place in high dimensions the search for the neighborhood of a new instance is problematic, since the majority of space is empty and neighbors can in fact be located far from each other. Furthermore, when noisy or irrelevant features are present it is likely that also irrelevant neighbors will be associated with a test instance. In this paper, we propose to use feature extraction in order to cope with the curse of dimensionality in the dynamic integration of classifiers. We consider classical principal component analysis and two eigenvector-based class-conditional feature extraction methods that take into account class information. Experimental results show that, on some data sets, the use of FEDIC leads to significantly higher ensemble accuracies than the use of plain dynamic integration in the space of original features.
5. Efficient Algorithm of Affine form Searching for Weakly Specified Boolean Function
   Piotr Porwik 277-291
   This paper presents the spectral method of recognition of an incompletely defined Boolean function. The main goal of analysis is fast estimation whether a given single output function can be extended to affine form. Furthermore, a simple extension algorithm is proposed for functions, for which the affine form is reachable. The algorithm is compared with other methods. Theoretical and experimental results demonstrate the efficiency of the presented approach.

77 (4) 2007

1. Typed Lambda Calculi and Applications 2005, Selected Papers - Preface i-i
2. The Completeness of Typing for Context-Semantics
   Thierry Coquand 293-301
   We present a variation of Hindley's completeness theorem for simply typed l-calculus. It is based on a Kripke semantics where the worlds are contexts, called context-semantics. This variation was obtained indirectly by simplifying an analysis of a fragment of polymorphic l-calculus [2]. We relate in this way works done in proof theory [4,14] with a fundamental result in l-calculus.
3. Tutorial Examples of the Semantic Approach to Foundational Proof-Carrying Code
   Amy P. Felty 303-330
   Proof-carrying code provides a mechanism for insuring that a host, or code consumer, can safely run code delivered by a code producer. The host specifies a safety policy as a set of axioms and inference rules. In addition to a compiled program, the code producer delivers a formal proof of safety expressed in terms of those rules that can be easily checked. Foundational proof-carrying code (FPCC) provides increased security and greater flexibility in the construction of proofs of safety. Proofs of safety are constructed from the smallest possible set of axioms and inference rules. For example, typing rules are not included. In our semantic approach to FPCC, we encode a semantics of types from first principles and the typing rules are proved as lemmas. In addition, we start from a semantic definition of machine instructions and safety is defined directly from this semantics. Since FPCC starts from basic axioms and low-level definitions, it is necessary to build up a library of lemmas and definitions so that reasoning about particular programs can be carried out at a higher level, and ideally, also be automated. We describe a high-level organization that involves Hoare-style reasoning about machine code programs. This organization is presented using two running examples. The examples, as well as illustrating the above mentioned approach to organizing proofs, is designed to provide a tutorial introduction to a variety of facets of our FPCC approach. For example, it illustrates how to prove safety of programs that traverse input data structures as well as allocate new ones.
4. Can Proofs be Animated by Games?
   Susumu Hayashi 331-343
   Proof animation is a way of executing proofs to find errors in the formalization of proofs. It is intended to be "testing in proof engineering". Although the realizability interpretation as well as the functional interpretation based on limit-computations were introduced as means for proof animation, they were unrealistic as an architectural basis for actual proof animation tools. We have found a game theoretic semantics corresponding to these interpretations, which is likely to be the right architectural basis for proof animation.
5. Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs
   Andreas Abel, Thierry Coquand 345-395
   Martin-Löf's Logical Framework is extended by strong S-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules is proven via a generic PER model on untyped terms. An algorithmic version of the framework is given through an untyped bh-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with h-equality on b-normal forms, which is shown equivalent to the algorithmic equality.
6. L³: A Linear Language with Locations
   Amal Ahmed, Matthew Fluet, Greg Morrisett 397-449
   We present a simple, but expressive type system that supports strong updates-updating a memory cell to hold values of unrelated types at different points in time. Our formulation is based upon a standard linear lambda calculus and, as a result, enjoys a simple semantic interpretation for types that is closely related to models for spatial logics. The typing interpretation is strong enough that, in spite of the fact that our core programming language supports shared, mutable references and cyclic graphs, every well-typed program terminates.
   We then consider extensions needed to model ML-style references, where the capability to access a reference cell is unrestricted, but strong updates are disallowed. Our extensions include a thaw primitive for re-gaining the capability to perform strong updates on unrestricted references. The thaw primitive is closely related to other mechanisms that support strong updates, such as CQUAL's restrict.
7. Rank 2 Intersection for Recursive Definitions
   Ferruccio Damiani 451-488
   Let |- be an intersection type system. We say that a term is |--simple (or just simple when the system |- is clear from the context) if system |- can prove that it has a simple type. In this paper we propose new typing rules and algorithms that are able to type (with rank 2 intersection types) recursive definitions that are not simple. Typing rules for assigning intersection types to (non-simple) recursive definitions have been already proposed in the literature. However, at the best of our knowledge, previous algorithms for typing recursive definitions in the presence of intersection types allow only simple recursive definitions to be typed. The rules and algorithms proposed in this paper are also able to type interesting examples of polymorphic recursion (i.e., recursive definitions rec {x=e} where different occurrences of x in e are used with different types). Moreover, the underlying techniques do not depend on particulars of rank 2 intersection, so they can be applied to other type systems.
8. Arithmetical Proofs of Strong Normalization Results for Symmetric l-calculi
   René David & Karim Nour 489-510
   We give arithmetical proofs of the strong normalization of two symmetric l-calculi corresponding to classical logic.
   The first one is the [`(l)]m[(m^~)]-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "call-by-value".
   The second one is the symmetric lm-calculus. It is the lm-calculus introduced by Parigot in which the reduction rule m¢, which is the symmetric of m, is added.
   These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical.
9. On the Expressiveness of Affine Programs with Non-local Control:
   The Elimination of Nesting in SPCF
   J. Laird 511-531
   We use a denotational semantics to show that every term in SPCF (a typed functional language with simple non-local control operators) is contextually equivalent to one which is typable in an affine typing system. Nested function calls and recursive definitions are not affinely typable, and so our result entails that they can be eliminated from SPCF without losing expressiveness.
   Our proof is based on the observation of Longley that every type of SPCF is a retract of a first-order type. We describe retractions of this kind in bistable biorder models of SPCF which are definable in the affine fragment. This allows us to transform an arbitrary SPCF term into an affine one by mapping it to a first-order term, obtaining an (affine) "normal form", and then projecting back to the original type.
   We show the flexibility of our approach by considering two variants of SPCF, a finitary, call-by-name version and a call-by-value version over the natural numbers. In the infinitary case, (in which we establish in addition that all instances of recursive definition may be replaced with iteration) our proof is based on an analysis of the relationship between SPCF definable functions and strategies for computing them sequentially.