Fme 2001 Formal Methods For Increasing Software Productivity 2001th Edition Jose N Oliveira

Fme 2001 Formal Methods For Increasing Software
Productivity 2001th Edition Jose N Oliveira
download
https://ebookbell.com/product/fme-2001-formal-methods-for-
increasing-software-productivity-2001th-edition-jose-n-
oliveira-57417436
Explore and download more ebooks at ebookbell.com

Here are some recommended products that we believe you will be
interested in. You can click the link to download.
Fme 2002formal Methodsgetting It Right International Symposium Of
Formal Methods Europe Copenhagen Denmark July 2224 2002 Proceedings
1st Edition Natarajan Shankar Auth
https://ebookbell.com/product/fme-2002formal-methodsgetting-it-right-
international-symposium-of-formal-methods-europe-copenhagen-denmark-
july-2224-2002-proceedings-1st-edition-natarajan-shankar-auth-2625448
Fme 2003 Formal Methods International Symposium Of Formal Methods
Europe Pisa Italy September 814 2003 Proceedings 1st Edition Kouichi
Kishida Auth
https://ebookbell.com/product/fme-2003-formal-methods-international-
symposium-of-formal-methods-europe-pisa-italy-
september-814-2003-proceedings-1st-edition-kouichi-kishida-
auth-2625452
Teaching Formal Methods Colognetfme Symposium Tfm 2004 Ghent Belgium
November 1819 2004 Proceedings 1st Edition Kungkiu Lau Auth
https://ebookbell.com/product/teaching-formal-methods-colognetfme-
symposium-tfm-2004-ghent-belgium-november-1819-2004-proceedings-1st-
edition-kungkiu-lau-auth-2625666

Lecture Notes in Computer Science 2021
Edited by G. Goos, J. Hartmanis and J. van Leeuwen

3
Berlin
Heidelberg
New York
Barcelona
Hong Kong
London
Milan
Paris
Singapore
Tokyo

Jos´e Nuno Oliveira Pamela Zave (Eds.)
FME2001:
FormalMethods
forIncreasing
SoftwareProductivity
International Symposium of Formal Methods Europe Berlin, Germany, March 12-16, 2001 Proceedings
13

Series Editors
Gerhard Goos, Karlsruhe University, Germany
Juris Hartmanis, Cornell University, NY, USA
Jan van Leeuwen, Utrecht University, The Netherlands
Volume Editors
Jos´e Nuno Oliveira
University of Minho, Computer Science Department
Campus de Gualtar, 4700-320 Braga, Portugal
E-mail: [email protected]
Pamela Zave
AT&T Laboratories Research
180 Park Avenue, Florham Park, New Jersey 07932, USA
E-mail: [email protected]
Cataloging-in-Publication Data applied for
Die Deutsche Bibliothek - CIP-Einheitsaufnahme
Formal methods for increasing software productivity : proceedings /
FME 2001, International Symposium of Formal Methods Europe, Berlin,
Germany, March 12 - 16, 2001. José Nuno Oliveira ; Pamela Zave (ed.).
- Berlin ; Heidelberg ; New York ; Barcelona ; Hong Kong ; London ;
Milan ; Paris ; Singapore ; Tokyo : Springer, 2001
(Lecture notes in computer science ; Vol. 2021)
ISBN 3-540-41791-5
CR Subject Classication (1998): F.3, D.1-3, J.1, K.6, F.4.1
ISSN 0302-9743
ISBN 3-540-41791-5 Springer-Verlag Berlin Heidelberg New York
This work is subject to copyright. All rights are reserved, whether the whole or part of the material is
concerned, specically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting,
reproduction on microlms or in any other way, and storage in data banks. Duplication of this publication
or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965,
in its current version, and permission for use must always be obtained from Springer-Verlag. Violations are
liable for prosecution under the German Copyright Law.
Springer-Verlag Berlin Heidelberg New York
a member of BertelsmannSpringer Science+Business Media GmbH
http://www.springer.de
© Springer-Verlag Berlin Heidelberg 2001
Printed in Germany
Typesetting: Camera-ready by author, data conversion by PTP-Berlin, Stefan Sossna
Printed on acid-free paper SPIN: 10782329 06/3142 543210

Preface
FME 2001 is the tenth in a series of meetings organized every eighteen months
by Formal Methods Europe (FME), an independent association whose aim is to
stimulate the use of, and research on, formal methods for software development.
It follows four VDM Europe Symposia, four other Formal Methods Europe Sym-
posia, and the 1999 World Congress onFormal Methods in the Development of
Computing Systems. These meetings have been notably successful in bringing to-
gether a community of users, researchers, and developers of precise mathematical
methods for software development.
FME 2001 took place in Berlin, Germany and was organized by the Com-
puter Science Department of the Humboldt-Universitat zu Berlin. The theme
of the symposium wasFormal Methods for Increasing Software Productivity.
This theme recognizes that formal methods have the potential to do more for
industrial software development than enhance software quality { they can also
increase productivity at many dierent points in the software life-cycle.
The importance of the theme is borne out by the many contributed papers
showing how formal methods can make software development more ecient.
There is an emphasis on tools that nd errors automatically, or with relatively
little human eort. There is also an emphasis on the use of formal methods to
assist with critical, labor-intensive tasks such as program design and test-case
generation.
The many application areas addressed in the various parts of the symposium
(tutorials, workshops, contributed papers, and invited papers) include smart
cards, avionic and satellite computers, nancial contracts, E-commerce, middle-
ware, security, telecommunications, and the FireWire standard. Many contribu-
tions involve multi-disciplinary teams of researchers coming from both industry
and academia. We are pleased to see this evidence of the spreading inuence of
formal methods.
In addition to the 32 papers selected for presentation by the program com-
mittee (out of 72 submissions involving authors from 25 countries), this volume
contains the abstracts of three invited talks:Lightweight Formal Methods,byDa-
niel Jackson (Laboratory for Computer Science, MIT);A Programming Model
for Wide-Area Computing, by Jayadev Misra (University of Texas at Austin);
andComposing Contracts: An Adventure in Financial Engineeringby Simon
Peyton Jones (Microsoft Research Ltd).
January 2001 Jos e Nuno Oliveira
Pamela Zave

Acknowledgements
We are very grateful to the members of the program committee and their referees
for their care and diligence in reviewing the submitted papers. We are also
grateful to the local organizers and the sponsoring institutions.
Program Committee
Eerke Boiten (UK)
Rick Butler (USA)
Lars-Henrik Eriksson (Sweden)
John Fitzgerald (UK)
Peter Gorm Larsen (Denmark)
Yves Ledru (France)
Dominique Mery (France)
Jayadev Misra (USA)
Richard Moore (Macau)
Friederike Nickl (Germany)
Tobias Nipkow (Germany)
Jose N. Oliveira (co-chair, Portugal)
Paritosh Pandya (India)
Nico Plat (The Netherlands)
Amir Pnueli (Israel)
Augusto Sampaio (Brazil)
Steve Schneider (UK)
Jim Woodcock (UK)
Pamela Zave (co-chair, USA)
Organizing Committee
Birgit Heene
Stefan Jahnichen (co-chair)
Axel Martens
Wolfgang Reisig (co-chair)
Thomas Urban
Tobias Vesper
Sponsoring Institutions
The generous support of the following companies and institutions is gratefully
acknowledged:
Humboldt-Universitat zu Berlin
GMD FIRST
Formal Methods Europe
Universidade do Minho
DaimlerChrysler AG
WIDIS GmbH Berlin
WISTA Management GmbH
External Referees
All submitted papers were reviewed by members of the program committee and a
number of external referees, who produced extensive review reports and without
whose work the quality of the symposium would have suered. To the best of
our knowledge the list below is accurate. We apologize for any omissions or
inaccuracies.

VIII Program Committee
Will Adams
Carlos Bacelar Almeida
Rajeev Alur
Tamarah Arons
Roberto Souto Maior de Barros
Pierre Berlioux
Didier Bert
Juan Bicarregui
Lynne Blair
Roland Bol
Paulo Borba
Lydie du Bousquet
Max Breitling
Dominique Cansell
Ana Cavalcanti
Michel Chaudron
David Cohen
Ernie Cohen
Jonathan Draper
Sophie Dupuy-Chessa
Peter van Eijk
Loe Feijs
Jean-Claude Fernandez
Dana Fisman
D. Galmiche
Max Geerling
Chris George
P. Gibson
N. Goga
Jan Friso Groote
Jan Haveman
Ian Hayes
Maritta Heisel
Rolf Hennicker
Dang Van Hung
Tomasz Janowski
He Jifeng
Adrian Johnstone
Cli B. Jones
Rajeev Joshi
Charanjit S. Jutla
Alexander Knapp
Nora Koch
Izak van Langevelde
Antonia Lopes
Gavin Lowe
Panagiotis Manolios
Andrew Martin
Stephan Merz
Anna Mikhailova
Oliver Moeller
Alexandre Mota
Paul Mukherjee
Kedar S. Namjoshi
David Naumann
George Necula
Gertjan van Oosten
Stephen Paynter
Andrej Pietschker
Nir Piterman
Marie-Laure Potet
Alexander Pretschner
Kees Pronk
Antonio Ravara
Jean-Luc Richier
Steve Riddle
Jan Rogier
Nick Rossiter
Stefan Romer
Thomas Santen
Jo~ao Saraiva
Emil Sekerinski
Kaisa Sere
Elad Shahar
Ofer Shtrichman
Kim Sunesen
Hans Tonino
Richard Treer
Alexandre Vasconcelos
Marcel Verhoef
Vladimir Zadorozhny
Irfan Zakiuddin
Lenore Zuck

Program Committee IX
Tutorials and Workshops
The following tutorials were scheduled for the two days preceding the research
symposium:
SDL 2001| J. Fischer, Andreas Prinz, and Eckhardt Holz (Humboldt-Uni-
versitat zu Berlin and DResearch Digital Media Systems GmbH)
Modeling for Formal Methods |Mcheal Mac an Airchinnigh, Andrew
Buttereld, and Arthur Hughes (University of Dublin)
From UML to Z, Support for Requirements Engineering with RoZ
| Yves Ledru and Sophie Dupuy (LSR/IMAG)
Beyond Model Checking: Formal Specication and Verication of
Practical Mission-Critical Systems| Ramesh Bharadwaj (Naval Re-
search Laboratory, USA)
We are grateful to all those who kindly submitted tutorial proposals. In addition,
two international workshops were co-located with the symposium tutorials:
First International Workshop on Automated Verication of Innite-
State Systems (AVISS'01)| organized by Ramesh Bharadwaj (Naval
Research Laboratory, USA) and Steve Sims (Reactive-Systems, Inc.)
Formal Approaches to the IEEE 1394 (FireWire) Identify Protocol
| organized by Carron Shankland, Savi Maharaj (University of Stirling),
and Judi Romijn (University of Nijmegen).
We thank the organizers of these events for their interest in sharing the atmos-
phere of the symposium.

Table of Contents
Lightweight Formal Methods::::::::::::::::::::::::::::::::::::::::1
Daniel Jackson
Reformulation: A Way to Combine Dynamic Properties andBRenement 2
F. Bellegarde, C. Darlot, J. Julliand, O. Kouchnarenko
Mechanized Analysis of Behavioral Conformance in the Eiel
Base Libraries:::::::::::::::::::::::::::::::::::::::::::::::::::::20
Steen Helke, Thomas Santen
Proofs of Correctness of Cache-Coherence Protocols::::::::::::::::::::43
Joseph Stoy, Xiaowei Shen, Arvind
Model-Checking Over Multi-valued Logics:::::::::::::::::::::::::::::72
Marsha Chechik, Steve Easterbrook, Victor Petrovykh
How to Make FDR Spin:
LTL Model Checking of CSP by Renement:::::::99
Michael Leuschel, Thierry Massart, Andrew Currie
Avoiding State Explosion for Distributed Systems with Timestamps::::::119
Fabrice Derepas, Paul Gastin, David Plainfosse
Secrecy-Preserving Renement:::::::::::::::::::::::::::::::::::::::135
Jan Jurjens
Information Flow Control and Applications { Bridging a Gap {::::::::::153
Heiko Mantel
A Rigorous Approach to Modeling and Analyzing
E-Commerce Architectures::::::::::::::::::::::::::::::::::::::::::173
Vasu S. Alagar, Zheng Xi
A Formal Model for Reasoning about Adaptive QoS-Enabled Middleware:197
Nalini Venkatasubramanian, Carolyn Talcott, Gul Agha
A Programming Model for Wide-Area Computing::::::::::::::::::::::222
Jayadev Misra
A Formal Model of Object-Oriented Design and GoF Design Patterns::::223
Andres Flores, Richard Moore, Luis Reynoso
Validation of UML Models Thanks to Z and Lustre::::::::::::::::::::242
Sophie Dupuy-Chessa, Lydie du Bousquet

XII Table of Contents
Components, Contracts, and Connectors for the Unied
Modelling Language UML:::::::::::::::::::::::::::::::::::::::::::259
Claus Pahl
An Integrated Approach to Specication and Validation of
Real-Time Systems:::::::::::::::::::::::::::::::::::::::::::::::::278
Adnan Sherif, Augusto Sampaio, Sergio Cavalcante
Real-Time Logic Revisited::::::::::::::::::::::::::::::::::::::::::300
Stephen E. Paynter
Improvements in BDD-Based Reachability Analysis of Timed Automata::318
Dirk Beyer
Serialising Parallel Processes in a Hardware/Software
Partitioning Context:::::::::::::::::::::::::::::::::::::::::::::::344
Leila Silva, Augusto Sampaio, Geraint Jones
Verifying Implementation Relations::::::::::::::::::::::::::::::::::364
Jonathan Burton, Maciej Koutny, Giuseppe Pappalardo
An Adequate Logic for Full LOTOS::::::::::::::::::::::::::::::::::384
Muy Calder, Savi Maharaj, Carron Shankland
Towards a Topos Theoretic Foundation for the Irish School of Constructive
Mathematics (M
|
c):::::::::::::::::::::::::::::::::::::::::::::::::396
Mcheal Mac an Airchinnigh
Faithful Translations among Models and Specications:::::::::::::::::419
Shmuel Katz
Composing Contracts: An Adventure in Financial Engineering:::::::::::435
Simon Peyton Jones
From Complex Specications to a Working Prototype. A Protocol
Engineering Case Study:::::::::::::::::::::::::::::::::::::::::::::436
Manuel J. Fernandez Iglesias, Francisco J. Gonzalez-Casta~no,
Jose M. Pousada Carballo, Martn Llamas Nistal,
Alberto Romero Feijoo
Coverage Directed Generation of System-Level Test Cases for the
Validation of a DSP System:::::::::::::::::::::::::::::::::::::::::449
Laurent Arditi, Hedi Boufaed, Arnaud Cavanie, Vincent Stehle
Using Formal Verication Techniques to Reduce Simulation and
Test Eort::::::::::::::::::::::::::::::::::::::::::::::::::::::::465
O. Laurent, P. Michel, V. Wiels
Transacted Memory for Smart Cards:::::::::::::::::::::::::::::::::478
Pieter H. Hartel, Michael J. Butler, Eduard de Jong, Mark Longley

Table of Contents XIII
Houdini, an Annotation Assistant for ESC/Java:::::::::::::::::::::::500
Cormac Flanagan, K. Rustan M. Leino
A Heuristic for Symmetry Reductions with Scalarsets::::::::::::::::::518
Dragan Bosnacki, Dennis Dams, Leszek Holenderski
View Updatability Based on the Models of a Formal Specication::::::::534
Michael Johnson, Robert Rosebrugh
Grammar Adaptation::::::::::::::::::::::::::::::::::::::::::::::550
Ralf Lammel
Test-Case Calculation through Abstraction::::::::::::::::::::::::::::571
Bernhard K. Aichernig
A Modular Approach to the Specication and Validation of an Electrical
Flight Control System::::::::::::::::::::::::::::::::::::::::::::::590
M. Doche, I. Vernier-Mounier, F. Kordon
A Combined Testing and Verication Approach for Software Reliability:::611
Natasha Sharygina, Doron Peled
Author Index:::::::::::::::::::::::::::::::::::::::::::::::::::629

Lightweight Formal Methods
Daniel Jackson
Laboratory for Computer Science
Massachusetts Institute of Technology
Cambridge, Massachusetts, USA
[email protected]
Abstract.Formal methods have oered great benets, but often at a
heavy price. For everyday software development, in which the pressures
of the market don't allow full-scale formal methods to be applied, a
more lightweight approach is called for. I'll outline an approach that is
designed to provide immediate benet at relatively low cost. Its elements
are a small and succinct modelling language, and a fully automatic anal-
ysis scheme that can perform simulations and nd errors. I'll describe
some recent case studies using this approach, involving naming schemes,
architectural styles, and protocols for networks with changing topologies.
I'll make some controversial claims about this approach and its relation-
ship to UML and traditional formal specication approaches, and I'll
barbeque some sacred cows, such as the belief that executability com-
promises abstraction.
J.N. Oliveira and P. Zave (Eds.): FME 2001, LNCS 2021, p. 1, 2001.
cSpringer-Verlag Berlin Heidelberg 2001

Reformulation: A Way to Combine
Dynamic Properties andBRenement
F. Bellegarde, C. Darlot, J. Julliand, and O. Kouchnarenko
Laboratoire d'Informatique de l'Universite de Franche-Comte
16, route de Gray, 25030 Besancon Cedex
Ph:(33) 3 81 66 64 52, Fax:(33) 3 81 66 64 50
fbellegar,darlot,julliand,[email protected],
Web :http://lifc.univ-fcomte.fr
Abstract.We are interested in verifying dynamic properties of reactive
systems. The reactive systems are specied by B event systems in a
renement development. The renement allows us to combine proof and
model-checking verication techniques in a novel way. Most of thePLTL
dynamic properties are preserved by renement, but in our approach,
the user can also express how a property evolves during the renement.
The preservation of the abstract property, expressed by aPLTLformula
F
1, is used as an assumption for proving aPLTLformulaF 2which
expresses an enriched property in the rened system. FormulaF
1is
veried by model-checking on the abstract system. So, to verify the
enriched formulaF
2, it is enough to prove some propositions depending
on the respective patterns followed byF
1andF 2. In this paper, we
show how to obtain thesesucientpropositions from the renement
relation and the semantics of thePLTLformulae. The main advantage
is that the user does not need to express a variant or a loop invariant to
obtain automatic proofs of dynamic properties, at least for nite state
event systems. Another advantage is that the model-checking is done on
an abstraction with few states.
Keywords:Verication ofPLTLproperties, Combination of proof and
model-checking, Renement development.
1 Introduction
Most properties of reactive systems [8,2,7] are dynamic. In our approach for the
design and verication, reactive systems are expressed byBnite state event
systems and their dynamic properties are formulated in the Propositional Linear
Temporal Logic [8] (PLTL). Recall that theBmethod is essentially a renement
design.
Our methodological approach as well as our verication techniques for ad-
dressing the introduction of dynamic constraints inB(see Fig. 1) is quite dif-
ferent from the propositions of J.{R. Abrial and L. Mussat in [2]. TheBevent
systems can be associated with nite or innite transition systems. InB, the
verication of invariants,dynamic invariantsand of liveness modalitiesleads to
J.N. Oliveira and P. Zave (Eds.): FME 2001, LNCS 2021, pp. 2{19, 2001.
cSpringer-Verlag Berlin Heidelberg 2001

Reformulation: A Way to Combine Dynamic Properties andBRenement 3
anduntiluses a proof technique which requires explicitvariantsandloop invari-
antsfrom the users.Variantsandloop invariantsare needed for the verication
of the liveness modalities. Moreover, a globalvariantis necessary for proving
that the renement introduces no live-lock. Our proposals deal only with the
specication and the verication of nite state systems but the specication and
the verication of anyPLTLproperty (safety, liveness, fairness) is possible.
Abstract
Event
System
Refined
Event
System
Verification
(Proof)
Verification
(Model-Checking)
Abstract
System
Properties
Refined
System
Properties
Refinement
(Model-Checking)
Refinement
Reformulation
Verification
Properties
System
New
Verification (Proof, Model Checking)
Fig. 1.Specication and verication approach
They dier from [2] in the four essential following points.
1. The dynamic properties are expressed inPLTL.
2. As for the events, the dynamic properties that are introduced at the abstract
level can be enriched through the renement. Then, they are formulated anew at the rened level. We say that the formula isreformulated.
3. The abstract dynamic properties are model-checked and theirreformulations
are veried by proof.
The motivation behind these propositions is threefold. First and above all,
we want to set the user free from looking for avariantand aloop invariant
when expressing dynamic properties. Second, we want to be able to use model- checking and proof for the verication in a way which utilizes them at their best. Third, the user can express its modalities freely using the expressive power of thePLTLlogic.
B+PLTLversusB+Modalities(see Point 1 above).In [2], J.{R.
Abrial and L. Mussat use three patterns of dynamic properties: thedynamic
invariantand the two modalitiesleads toanduntil.Ifpandqare propositional
predicates, thedynamic invariantshave the same expressive power as the set
ofPLTLformulae2(p)q). The modalities have the same expressive power
as a fragment of thePLTLusing the two kinds of properties2(p)}q), and
2(p)(pUq)). Moreover, besides the instances forpandq, the user has to
specify avariant, often aloop invariant, and a list of the events which may be
taken during the loop.

4 F. Bellegarde et al.
We use thePLTLfuture operatorsAlways,Next,Eventually, andUntil(de-
noted respectively by2,,}, andU) with the following meaning. For a path
,
{2pmeans that the propertypholds in each state of;
{pmeans that the propertypholds in the next state;
{}pmeans that there exists a state in the future which satisesp;
{pUqmeans thatpholds untilqeventually happens.
Model-Checking and Proof (see Points 3 above). We choose thePLTL
logic because its verication can be done byPLTLmodel-checking [5] which is
entirely automatic for the totality of the logic. The main drawback is that it
cannot handle very or innite state systems. A solution for large nite systems
may consist of using jointly proof and model-checking. So, the model-checking
explosion is avoided as well as the requirement consisting in providing clues such
asvariantsandloop invariantsto a theorem prover. To better explain how we
propose to join both techniques to verify the reformulated properties consider
Fig. 1.
First, the user species the abstract event system with its invariant and its
dynamic properties expressed inPLTL. The invariant is proof-checked as in
B. The dynamic properties are model-checked on the event system operational
model, i.e., on the set of paths of a nite state transition system with a small
number of states.
Second, the user species its renements introducing new variables. The re-
lation between the set of statesS
2of the rened system and the set of statesS 1
of the abstract system is expressed by agluing invariant. New events are intro-
duced, old events are formulated once more, newPLTLformulae are introduced,
and oldPLTLformulae are formulated anew.
We do not want to use thePLTLmodel-checking again for the verication of
the reformulated properties. So, we propose to use proof techniques, but without
requiring aloop invariantand of avariant. In the paper, we present two kinds of
propositions which are associated systematically according to the shapes (called
renement patterns) of the abstractPLTLformula and the rened formula. The
rst kind|a weak form, includes propositional sub-formulae and the invariants
of the event systems. When they are valid, we know that the rened formula
holds. The failure does not mean that the rened formula does not hold. So, the
second kind|a strong form, includes either the abstract or the rened events.
Again, the success means that the rened formula holds but, from a failure, we
cannot conclude. Therefore, these propositions aresucient conditionsand not
proof obligations.
In the paper, we show that if these propositions (weak or strong) are valid,
then the reformulated properties hold without the help of neither an user-given
variantnor aloop invariant.
Reformulation versus Preservation (see Point 2 above). In [2], the
modalitiesleads toanduntilwhich hold on the abstract paths are preserved

Reformulation: A Way to Combine Dynamic Properties andBRenement 5
on the rened paths. However,dynamic invariants, which could be expressed by
an instance of thePLTLpattern2(p)q), are not preserved on the rened
paths since new events may not verify thedynamic invariant. Moreover, because
the new events are interwovenamong the old ones, the rened system does not
satisfy the pattern2(p)q) but it satises an instance of thePLTLpattern
2(p)}q)|a weaker formula. More generally, the preservation technique does
not allow the user to indicate how the new events are interwovenamong the old
events. However, the reformulation can do it. For example, the reformulation of
thePLTLpattern2(p
1)q 1)bythePLTLpattern2(p 2)q 2), allows us
to specify that it is forbidden to introduce some of the new events before the
old events which are enabled whenp
1holds. The reformulation of the pattern
2(p
1)q 1) by the pattern2(p 2)(r 2Uq2)) allows introducing only the new
events which maintainr
2. So, the purpose of the reformulation of a property is
that the formula of the rened property species explicitly how the new events
can be interwovenamong the old events. Therefore, the reformulated formula
may be richer than the preserved formula. The eect of a reformulated formula
compares with the eect of a gluing invariant in the following manner. Agluing
invariantspecies a relation between the rened and the abstract states whereas
a reformulated formula, together with thegluing invariant, species a relation
between the rened and the abstract paths of the operational model. It is redun-
dant with the expression of the events but we think that it is important that the
design allows such redundancies in a specication so that the verication can
exploit them.
Paper Organization.The paper is organized as follows. Section 2 illustrates
our approach on an example. After a short presentation of our renement re-
lation, we explain how to verify thereformulateddynamic properties through
renement in Section 3. Finally, we situate our concerns and give some ideas
about future works in Section 4.
2 Example
In this section, we introduce a robot as an example. We will examine the oper-
ational specication, and then, we will express some dynamic properties to be
veried on this system.
2.1 Operational Description
Figure 2 shows the physical system. The robot must move some parts from the
arrival device(calledAD) to one of theexit devices(called resp.LEDandRED
for the left and right exit devices) using thecarrier device(calledCD).
Here, we show the abstract specication as well as two further levels of rene-
ment calledrst renementandsecond renement. We express the specications
using aBevent system syntax extended withPLTL. Notice that the variables
are annotated with a number corresponding to the level of renement (here: 0,
1 and 2).

6 F. Bellegarde et al.
LED = Left Exit Device
RED = Right Exit Device
CD = Carrier Device
AD = Arrival Device
LED RED
AD
CD
Fig. 2.Physical system
Abstract Specication.The very abstract specication only formalizes the
transportation of the parts ignoring the arrival and exit devices and the car-
rier device movements which will be considered in further renements. In other
words, we only observe the carrier device state. Figure 3 gives the operational
semantics of the abstract level specication described as the event system below
(for theBsyntax, please see [1]). There are two events:
{Load: The carrier device takes a part, then it is busy (valueb);
{Unload: The carrier device drops a part, then it is free (valuef).
EVENT SYSTEM ROBOT 0
SETS:DEVICE
STATE=ff,bg
VARIABLES: CD
0
INVARIANT: CD 02DEVICE
STATE
INITIALIZATION: CD
0:=f
EVENTS:
Load ^=SELECTCD
0=fTHENCD 0:=bEND;
Unload ^=SELECTCD
0=bTHENCD 0:=fEND
END
Unload Load
Fig. 3.Transition system for the abstract level

Reformulation: A Way to Combine Dynamic Properties andBRenement 7
First Renement.We consider now the left and right exit devices. The vari-
ables of the abstract and the rened specications are linked together by agluing
invariant. We observe two new events (LEvacandREvac) which set the exit
devices free. These events can happen whenever the exit devices are busy. In
the rened specication, the old events keep the same labels. Notice that the
guards of the old events (e.g.Unload) are strengthened. Also, notice that when
both exit devices are free, the carrier device unloads a part nondeterministically
either toward the left exit device or toward the right exit device.
The transition system in Fig. 4 shows the rst renement operational seman-
tics. We can notice that if we group the states according to the gluing invariant,
we obtain twomodules(one where in each state the carrier device is empty and
one where it is busy) corresponding to the two states of the abstract level.
EVENT SYSTEM ROBOT 1REFINES ROBOT 0
VARIABLES: LED 1, RED1,CD1
INVARIANT:
LED
12DEVICE
STATE^RED 12DEVICESTATE^CD 1=CD0
INITIALIZATION: LED 1:=fkRED 1:=fkCD 1:=f
EVENTS: /* Old events */ Load ^=SELECTCD
1=fTHENCD 1:=bEND;
Unload ^=SELECT(LED
1=f_RED 1=f)^CD 1=b
THEN IFLED
1=bTHENRED 1:=b
ELSE IFRED
1=bTHENLED 1:=b
ELSE CHOICE LED
1:=b
ORRED
1:=bEND
END
END kCD
1:=f
END;
/* New events */ LEvac ^=SELECTLED
1=bTHENLED 1:=fEND;
REvac ^=SELECTRED
1=bTHENRED 1:=fEND
ENDROBOT
1
Second Renement.Now, we observe two new events (LRotateandRRotate)
which change the carrier device side which is registered in the variableCDS.
The side value is either left|denotedl, or right|denotedr. We remove the
nondeterminism by giving priority to the left exit device whenever possible|
this for minimizing the carrier device movements, i.e., we do not unload on the
right exit device if the left one is free.
EVENT SYSTEM ROBOT 2REFINES ROBOT 1
SETS:SIDE=fl,rg
VARIABLES: LED
2, RED2,CD2, CDS2

8 F. Bellegarde et al.
LED = f /\
CD = f /\
RED = b
LEvac
Load
REvac
UnloadUnload
LEvac REvac
Load Load
REvac
REvacLEvac
UnloadUnload
Load
LEvac
Legend:
Fig. 4.First renement transition system
INVARIANT:
LED
2=LED1^RED 2=RED1^CD 2=CD1^CDS 22SIDE^
(CDS
2=r)(CD 2=f_RED 2=f))
INITIALIZATION: LED
2:=fkRED 2:=fkCD 2:=fkCDS 2:=l
EVENTS:
/* Old events */
Load ^=SELECTCD
2=f^CDS 2=lTHENCD 2:=bEND;
Unload ^=SELECTCD
2=b^((LED 2=f^CDS 2=l)_
(RED
2=f^CDS 2=r^LED 2=b))
THEN IFLED
2=f^CDS 2=lTHENLED 2:=b
ELSERED
2:=b
END
kCD
2:=f
END;
LEvac ^=SELECTLED
2=bTHENLED 2:=fEND;
REvac ^=SELECTRED
2=bTHENRED 2:=fEND;
/* New events */
LRotate ^=SELECTCDS
2=r^(CD 2=f_LED 2=f)
THENCDS
2:=l
END;
RRotate ^=SELECTCDS
2=l^CD 2=b^LED 2=b^RED 2=f
THENCDS
2:=r
END
END

Reformulation: A Way to Combine Dynamic Properties andBRenement 9
Figure 5 shows the second renement transition system. We can notice that
if we group the states according to the gluing invariant, we obtain eight modules.
REFINEMENT
FIRST
Load
RRotate
LRotate
Load
LRotate LRotate
Unload
Load
LEvac
LEvac
LEvac
Load
LRotate
REvac
LEvac
Unload LEvac
REvac
REvac
Unload
REvac
LEvac
LEvac
LRotate
REvac REvac
LEvac
Load
REvac
UnloadUnload
LEvac REvac
Load Load
REvac
REvacLEvac
UnloadUnload
Load
LEvac
Fig. 5.Second renement transition system
2.2 Dynamic Properties
We want to express some dynamic properties to be veried on the systems pre-
viously described.
Dynamic Properties of the Abstraction.The carrier device should imme-
diately unload. This is expressed by Formula 1 which can be read as follows: \At
any time, if the carrier is busy, it is free in the next state".
2(CD
0=b)(CD 0=f)) (1)
Dynamic Properties for the First Renement. The previous property is
reformulated either into Formula 2 or into Formula 3.
2(CD
1=b)}(CD 1=f)) (2)
2(CD
1=b)}(CD 1=f^(LED 1=b_RED 1=b))) (3)

10 F. Bellegarde et al.
Formula 2 considers that any event which does not modify the carrier state
may happen before unloading. If the renement holds, Formula 2 holds without
any further verication since any instance of a formula2(p) q) renes
into the same instance of2(p)}q). So, the reformulation is unnecessary.
However, Formula 3 expresses more about how the unloading may happen. It
says explicitly that a busy carrier device will eventually unload on one of the
two exit devices. So, the reformulation allows us to be more accurate.
Remark 1.In both cases, the temporal operatorbecomes a}in the refor-
mulation. We say that the reformulation follows a renement pattern (2(p)
q);2(p)}q)), for short}.
We also have the two following new properties:
{The carrier device holds the part until one of the exit devices becomes free.
2(CD
1=b
)((CD
1=b)U(CD 1=b^(LED 1=f_RED 1=f))))
(4)
Formula 4 could also be considered as a reformulation of the abstract prop-
erty 1.
{If the three devices are busy, then, the carrier device remains busy. In other
words, only the evacuation is allowed.
2((CD
1=b^LED 1=b^RED 1=b))(CD 1=b)) (5)
Dynamic Properties for the Second Renement. The above properties
can be reformulated as follows by taking the carrier device side into considera-
tion.
{Formula 3 is reformulated into Formula 6, following a}}pattern:
2(CD
2=b)}(CD 2=f^((LED 2=b^CDS 2=l)_
(RED
2=b^CDS 2=r))))
(6)
The enrichment of Formula 3 in Formula 6 consists in expressing that he
carrier device is turned to the side of the previous unloading".
{Formula 4 is reformulated into Formula 7, following aUUpattern:
2((CD
2=b^LED 2=b^CDS 2=l))((CDS 2=l^CD 2=b)
U(CDS
2=l^CD 2=b^(LED 2=f_RED 2=f))))
(7)
It can be read as: \If the carrier device is busy and directed toward its left,
it stays directed toward the left until it can turn to the right.
{Formula 5 is reformulated into Formula 8. It follows a pattern by ex-
pressing that theneweventsLRotateandRRotatemust preserve the.
2((CD
2=b^LED 2=b^RED 2=b)
)(CD
2=b))
(8)
It can be read as: \The carrier device must stay busy when rotating".

Reformulation: A Way to Combine Dynamic Properties andBRenement 11
The next section describes how to deduce invariants providing sucient ver-
ication conditions from thePLTLproperty syntax at both the rened and the
abstract levels together with the path renement relation.
3 Reformulated Dynamic Property Verication
In this section, we explain how to verify the reformulated dynamic properties
through renement. We suppose that the systemTS
2of state spaceS 2renes
the abstract systemTS
1of state spaceS 1and we exploit this renement to show
that if a propertyP
1holds on the abstract system then a reformulated property
P
2holds on a rened system.
We hope to avoid thePLTLproperty model-checking explosion which is likely
to happen during the renement by providing sucient conditions to verify the
reformulatedPLTLpropertyP
2using thatholds betweenTS 2andTS 1and
P
1holds onTS 1as assumptions.
These conditions are rst-order predicate formulae where the predicate do-
mains are limited to nite sets so that these conditions are easily decidable by
any theorem prover. Moreover, the conditions depend on the formulation of the
PLTLproperty at both levels.
We determine two kinds of conditions. The rst kind does not take into
account the events. These conditions are often too weak to prove thePLTL
formulae. So, we consider how the new events are interwovenamong the old
events to exhibit stronger conditions. Therefore, as in theBproof obligations
for renement, these last conditions are formulated using guards and generalized
substitutions of the events.
3.1 About Renement
We use transition systems as operational semantics of theBevent systems be-
cause of thePLTLsemantics. At the abstract level, aPLTLpropertyPis veried
for the event system by model-checking on a transition system which is its op-
erational model. This supposes that the set of states of this transition system is
nite.
In this section, we give an intuitive presentation of a renement relation
between the set of statesS
2of the rened transition systemTS 2and the set
of statesS
1of the abstract transition systemTS 1which determines a relation
between the paths of the transition systems modeling the corresponding event
systems. This relation has been studied thoroughly in [4].
As inB, the important assumption is that the new events do not take control
forever. However, in our approach, this is veried by a model state enumeration.
The renement verication is linear in the number of states of the rened system.
This way we prevent the state explosion coming from thePLTLmodel-checking
itself.
As for the renement inB, the conjunction of the abstract system invariant
I
1and the gluing invariantI 2determines a relationbetween the rened and

12 F. Bellegarde et al.
abstract states. The renement relationrestrictstaking into account that
the new events do not take the control forever, and that non-determinism may
decrease. The relationbetween states implies a relation between the rened
paths and some abstract paths of the transition systems. Figure 6 gives an
example of two related paths. As usual, thePLTLmodel-checking is based on the
labeling of each state by a set of the propositions holding on it. By the renement
denition from [4], it is very important to ensure that any event which is taken
on the abstract path is also eventually taken on the rened path preceded by
some new events.

en1
//
en
//
//

77oooooooooooooo

??

en1
//

OO
//

OO

__@
@
@
@
@
@
@

en
//

ggOOOOOOOOOOOOOO

gg OOOOOOOOOOOOOO
Fig. 6.Path renement example
3.2 Renement and Dynamic Properties
The dynamic properties that can be expressed inBevent systems are
{either a dynamic invariant which indicates how the variables of the system
are authorized to evolve; this corresponds roughly to aPLTLformula in-
volving the next operator as2(p)q);
{or theBmodalities which havePLTLequivalences as the patterns2(p)
}q) and2(p)(pUq)).
Generally, aPLTLformula following the pattern2(p
1)q 1) is formulated
again at a rened level either as the pattern2(p
2)q 2)or2(p 2)}q 2)or
2(p
2)(r 2Uq2)). It can be a more complicated expression. We call arenement
patterna pair of aPLTLpattern and its reformulated pattern. Notice that in a
given pattern, the variables are propositional variables.
Our approach allows the user to have more exibility to express properties
through renement than inB(where the modalities are onlypreservedand
cannot be expressed again).
On the one hand, the preservation of dynamic invariant through theBre-
nement seems to correspond to the renement pattern

2(p
1)q 1);2(p 2)
}q
2)

(for short,}).
On the other hand, theBrenement preserves the modalities patterns.
Again the reformulation oers more possibilities. First, the patternUis2(p
1)
(r
1Uq1)) whereas theBmodalityuntilcorresponds to a pattern2(p 1)
(p
1Uq1)). Second, a patternUmay evolve into a pattern}. Third, the refor-
mulation allows enriching gradually a property through renement. In contrast,

Reformulation: A Way to Combine Dynamic Properties andBRenement 13
when a propertyPdoes not need to be enriched, it is preserved by renement
so that, in such a case, it is useless to reformulatePduring further renements.
Notice that it is inconceivable that a pattern}evolves into a pattern. The
direction of the implication between the patterns of the pair is naturally mirrored
by the direction of the renement. We have discussed the pattern evolution
through renement in [6].
The sucient proof conditions are deduced from thePLTLrenement pat-
tern semantics. So, we are not limited to a small set of renement patterns. Our
experience shows that in most applications the same few renement patterns
are often used. However, a small number of more complicated renement pat-
terns may be novel to a particular application but it is generally easy to build a
corresponding sucient condition set as it is shown in the next section.
3.3 Weak Sucient Conditions
Consider the renement patternUU. Suppose a formula of pattern2(p
1)
(r
1Uq1)) holds on the paths of the abstract transition systemTS 1.Wewantto
have sucient conditions for the pattern2(p
2)(r 2Uq2)) holding on the paths
of a rened transition systemTS
2.
From the semantics ofUand from the path renement relation as shown in
Fig. 6, we deduce the following set of sucient conditions.
{A beginning condition.Assumep
2is satised on a states 2, ands 1be the
abstract state such thats
2together withs 1satisfyI 2^I1. Then,p 1must
be satised bys
1. From that we deduce a rst conditionp 2^I2^I1)p1.
{A maintenance condition.The propositionr
1holds on each statesof any
path of the abstract system beginning ins
1before the satisfaction ofq 1. So,
r
2must also hold on each states
0
of any path of a rened system beginning
ins
2before the satisfaction ofq 2. By renement,sands
0
satisfyI 2^I1.
From that we deduce a second conditionr
1^I2^I1)r2.
{An ending condition.On any path afters
1there exists a statetsatisfying
q
1. So, ifq 2holds on a statet
0
such thattandt
0
satisfyI 2^I1, we are done.
We deduce the third conditionq
1^I2^I1)q2.
We see that we have two kinds of implications, one from an abstract system
property to a rened system property (either for an ending condition or a main-
tenance condition), and the other from a rened system property to an abstract
system property (for a beginning condition) (see Fig. 7).
We now give theorems providing a building block for a beginning condition.
Theorem 1.Given an abstract transition systemTS
1of state spaceS 1, and
a transition systemTS
2of state spaceS 2reningTS 1, letI 1be the invariant
ofTS
1, and letI 2be the gluing invariant. Each states 1(2S 1)glued with a
states
2(2S 2)on which a propositionp 2holds satises a propositionp 1if the
conditionp
2^I2^I1)p1holds ons 2^s1.

14 F. Bellegarde et al.

p1
a
//

r1
a
//
a
//

q1
p2
==
z
z
z
z
z
z
z
z

a
beginning building block
//
r2
//
OO
r2
maintenance building block
//
aaD
D
D
D
D
D
D
D

r2
a
//
hhQQQQQQQQQQQQQQQ
a
ending building block
//
q2
aaD
D
D
D
D
D
D
D
Fig. 7.Building blocks
Proof.Immediate by the following. Lets 22S2be a state satisfyingp 2. Let
s
12S1be a state glued withs 2. Then,s 2ands 1satisfyp 2^I1^I2. Since
p
2^I2^I1)p1, the propertyp 1which contains only variables ofTS 1, holds
ons
1.
Theorem 2.The condition stated by Theorem 1 is a building block for a begin-
ning condition of any renement pattern

2(p
1)Q 1);2(p 2)Q 2)

whereQ 1
andQ 2are PLTL formulae.
Proof.Immediate by the following. If a rened path begins in a state satisfying
p
2then it is necessarily glued with all the states inS 1satisfyingp 1.
We propose another building block either for a maintenance condition or for
an ending condition.
Theorem 3.Given an abstract transition systemTS
1and a transition system
TS
2reningTS 1, letI 1be the invariant ofTS 1, and letI 2be the gluing invari-
ant. Each states
2(2S 2)glued with a states 1(2S 1)on which a propositionq 1
holds satises a propositionq 2if the conditionq 1^I2^I1)q2holds ons 2^s1.
Proof.The proof is the same as for Theorem 1.
Theorem 4.The condition stated by Theorem 3 is a building block for an ending
condition of any renement pattern

2Q
1;2Q 2

whereq
1is an eventuality which
occurs in the PLTL formulaQ
1andq 2is an eventuality which occurs in the
PLTL formulaQ
2.
Proof.Immediate by the following. If an abstract states
1satisfyingq 1occurs
in a path ofS
1then all the states inS 2glued withs 1are compelled to satisfy
q
2.
As a consequence of Theorem 3, a maintenance condition can be deduced
according to the following argument. Lets
1be a state inS 1for whichr 1holds.
In a path ofTS
2, all the states which begin a transition reningskip(these
transitions are labeled by new events) that are glued withs
1verifyr 2. Notice
how important are thenon-divergenceand thelack of new deadlockclauses
of the renement relation for reaching the ending condition. However, it may be
too weak when new events appear since, in this case, the condition forcesq
2to

Reformulation: A Way to Combine Dynamic Properties andBRenement 15

p1
a
//

q1
p2;r2;:q2
//
88rrrrrrrrrr

r2;:q2
//
OO
r2;:q2
a
//
eeKKKKKKKKKK

q2
ccH
H
H
H
H
H
H
H
H
Fig. 8.PatternU
be true after each of these new events up until the occurrence of the next old
event.
We now have a way to construct the set of weak sucient conditions associ-
ated to one of the following often used renement patterns,U,},UU,
U},}}. For instance, the set of weak sucient conditions for the renement
pattern

2(p
1)q 1);2(p 2)(r 2Uq2))

is (see Fig. 8)
p
2^I2^I1)p1;a beginning condition
p
1^I2^I1)r2;a maintenance condition
q
1^I2^I1)q2;an ending condition
Consider the following dynamic property for the event system from Section 2.
If the carrier device is busy, and so are both exit devices then, in the next state,
the carrier device remains busy while one of the exit devices becomes free.
2((CD
1=b^LED 1=b^RED 1=b))((CD 1=b)
^(LED
1=f_RED 1=f)))
(9)
Notice that this implies Property 5 from Section 2.2. The above property is
reformulated into
2((CD
2=b^LED 2=b^RED 2=b))((CD 2=b)
U(CD
2=b^(LED 2=f_RED 2=f))))
(10)
because of the new events. The above set of weak sucient conditions is enough
to ensure the satisfaction of the reformulated property.
Moreover, the building blocks can also be used to deduce weak sucient
conditions for more complex renement patterns. Consider, for example, a re-
nement pattern

2(p
1)(r 1Uq1));2(p 2)}(r 2)r2Uq2))

. Its set of weak
sucient conditions is the following:
p
2^I2^I1)p1;a beginning condition
r
1^I2^I1)r2;a maintenance condition
q
1^I2^I1)q2;an ending condition
Unfortunately, some of these building blocks are often too weak for the proof
because they do not express the semantics of the renement patterns precisely
enough. The next section presents strong sucient conditions which are used in

16 F. Bellegarde et al.
our verication process when the weak sucient conditions fail in proving an
instance of a renement pattern.
Obviously, the cause of the failure may not come from the conditions but
either from the incorrectness of the rened formula (error of expression or error
in the pattern evolution), or even from the incorrectness or the insuciency of
the gluing invariant. The problem with the invariant happens only if the modular
renement relation does not hold. So, the renement verication eliminates this
cause of failure.
3.4 Strong Sucient Conditions
In the failure case, we have to try a strong sucient condition based on the
new events (reningskip) interwovenamong the old events. For example, with
the renement pattern}followed by Formula 1 and its reformulation into
Formula 3, the proof of the set of weak conditions fails for the ending condition
q
1^I2^I1)q2. Then, the weak ending condition has to be replaced by the
following strong ending sucient condition:
8a2OldEvents;p
1^G1a^G2a^I1^I2)[S 2a]q2
whereS 2ais a generalized substitution of an old eventain a rened system,G 2a
is its guard, andG 1ais the guard of the eventain the abstract system. In other
words, each old eventaenabled by a rened states
2which satisesr 2and is
glued with an abstract states
1satisfyingp 1, changess 2into a state satisfying
q
2.
The above condition also can be used as an ending condition for the rene-
ment patternU. It is used in proving Formula 4 as a reformulation of For-
mula 1. However, for the patternU, the left-hand side of the implication often
needs to be strengthened with the conjunction ofr
2to better t the semantics
ofU.
Strong sucient conditions are also required by the persistence of thePLTL
operatorin a renement pattern.
The persistence of thePLTLoperatorin a pattern evolution.We can
imagine three plausible renement patterns coming from the abstract pattern
p
1)q 1.
{The more likely the patternevolves into eventuality patterns either}(e.g
Formula 1 reformulated into Formula 3) orU(e.g. Formula 1 reformulated
into Formula 4) because of transitions reningskip.
{However, in a few cases, it may happen that the property is not concerned
with the new events. For instance, Formula 5 of the second renement is
satised by both of the new eventsLRotateandRRotate. With this point of
view, it is reformulated into Formula 8.
For apersistence, the weakest set of sucient conditions we can build is
composed of the weak beginning condition, the weak ending condition, and a

Reformulation: A Way to Combine Dynamic Properties andBRenement 17
condition saying that no new event can precede an old event concerned with.
This condition is
8a2NewEvents;(p
1^I1^I2)):G a
whereG ais the guard of an eventa. Therefore, any states 2satisfyingp 2must
not satisfy a guard of a new event which is sucient to ensure the persistence
of:p
2.
More about strong sucient conditions.Let us examine strong sucient
conditions for the pattern renementUUfollowed by Formula 4 and its reformu-
lation into Formula 7 as expressed in Section 2.2. The following strong ending
condition
8a2OldEvents;r
1^:q 1^r2^:q 2^G1a^G2a^I1^I2)[S 2a]q2
is easily built for this renement pattern (see Fig. 9). However, this condition is
likely to fail because of the old events which may be taken before theUends.
So, the renement patternUUrequires the following stronger sucient ending

p1;r1
:q1
a1
//
r1
:q1
a2
//

q1

:q2
p2;r2
//
55llllllllllllllll

:q2
r2
//
<<
x
x
x
x
x
x
x
x

:q2
r2
a1
//
OO

:q2
r2
//
OO

:q2
r2
//
bbD
D
D
D
D
D
D
D

:q2
r2
a2
//
hhRRRRRRRRRRRRRRRR

q2
hhQQQQQQQQQQQQQQQQQ
Fig. 9.PatternUU
condition which eliminates from the condition the events which might be taken
before theUends, i.e., the events which do not change the abstract state to
an abstract state which satisesq
1. For that, it is enough to strengthen the
implication with the conjunction of [S
1a]q1.
8a2OldEvents;
r
1^:q 1^r2^:q 2^G1a^G2a^I1^I2^[S1a]q1)[S 2a]q2
This stronger sucient ending condition proves the reformulated Formula 7 of
Section 2.2. The renement pattern}}follows the same ending stronger su-
cient condition, condition which allows proving that, assuming the satisfaction
of Formula 3, its reformulation by Formula 6 holds.
Notice that the strong sucient conditions are universally quantied on ei-
ther the set of the new events or the set of the old events of a rened system.
As for the deduction of the weak sucient conditions, we can exhibit building
blocks but they take into account the guards and the generalized substitutions
of the involved events. Again, for a given renement pattern, we get a construc-
tive way to nd the set of strong sucient conditions by using building blocks
according to their respective semantics.

18 F. Bellegarde et al.
3.5 Dynamic Properties Reformulation Versus Variants and Loop
Invariants
In this section, we have shown that the verication ofPLTLreformulation of
the dynamic properties can be fully automatic for nite state systems using no
variant and no loop invariant.
Given aPLTLformulaP
1and its reformulationP 2, we get a systematic
construction for nding a set of propositions (building blocks) which suces to
ensure that the rened property holds on the rened system. So, failure does not
mean that the property is false. There are two main causes of failure:
{either the gluing invariant is too weak,
{or the property is false, but may be only outside the reachable state set.
Notice that it is the same as inBwhere an invariant which does not hold on
the whole state space could be true on the reachable state space.
The sucient conditions can be viewed as another way to use the preser-
vation ofP
1by renement as an assumption to verifyP 2. Formulating again a
property through renement is useful for three reasons. First, in order to estab-
lish the gluing invariant, the user can have a path renement style of reasoning
and not only a variable connection one. Second, it allows us to deal with the
model-checking explosion problem since we avoid to model-check the reformu-
lated property by proving either weak or strong sucient conditions. Third, it
opens up an original solution to combine proof and model-checking techniques.
This solution is based on renement.
4 Conclusion and Perspectives
We have proposed a distinctive approach for the verication of nite state re-
active systems. The specications are expressed asBnite state event systems,
i.e., the variables range over nite domains. A signicant number of reactive sys-
tem, particularly communication and synchronization protocols, are in essence
nite state systems. Moreover, the renement design of event systems requires
a decreasing variant for verifying that the new events|the events introduced in
the specication during the renement, do not take control forever. Our goal is
to liberate the design from such features. For that purpose, the verication con-
sists in confronting the labeled transition system which models the nite state
specication with its dynamic properties expressed byPLTLformulae. This can
be done automatically by model-checking without additional features. Moreover,
the renement has to relate an abstract transition system and its renement by
themodular renement relationwhich is easily veried algorithmically in the
particular case of nite state systems. The combination of proof techniques and
model-checking relies on a distinction betweenreformulatedandnew properties,
the rst being veried by a proof technique and the second, by model-checking.
Reformulating a property through renement is useful for three reasons.
First, in order to establish the gluing invariant, the user can have a path re-
nement style of reasoning and not only a variable relationship one. Second,

Reformulation: A Way to Combine Dynamic Properties andBRenement 19
it allows us to deal with the model-checking explosion problem since we avoid
model-checking the reformulated property by proving either weak or strong suf-
cient conditions. Third, it opens up a peculiar approach for combining proof
and model-checking techniques. This approach is based on renement.
We are currently improving and completing our toolkit (described in [3]) so
that we can validate the verication process on larger examples. This is also
needed for validating the methodology on industrial size applications. This is
essential for our claim aboutreformulated/new properties. Furthermore, we are
extending some of the above ideas from nite state systems to a class of param-
eterized systems which are innite state systems. The idea is that the abstract
system can be nite state whereas the renements may be innite state systems.
References
1. J.-R. Abrial.TheBBook. Cambridge University Press - ISBN 0521-496195, 1996.
2. J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. InSecond
Conference on the B method, France, volume 1393 ofLecture Notes in Computer
Science, pages 83{128. Springer Verlag, April 1998.
3. F. Bellegarde, C. Darlot, J. Julliand, and O. Kouchnarenko. Reformulate dynamic
properties during B renement and forget variants and loop invariants. InProc. Int.
Conf. ZB'2000, York, Angleterre. Springer-Verlag, August 2000. LNCS to appear.
4. F. Bellegarde, J. Julliand, and O. Kouchnarenko. Ready-simulation is not ready to
express a modular renement relation. InProc. Int. Conf. on Fundamental Aspects
of Software Engineering, FASE'2000, volume 1783 ofLecture Notes in Computer
Science, pages 266{283. Springer-Verlag, April 2000.
5. G. Holzmann.Design and validation of protocols. Prentice Hall software series,
1991.
6. J. Julliand, F. Bellegarde, and B. Parreaux. De l'expression des besoins a
l'expression formelle des proprietes dynamiques.Technique et Science Informa-
tiques, 18(7), 1999.
7. L. Lamport. A temporal logic of actions.ACM Transactions On Programming
Languages And Systems, TOPLAS, 16(3):872{923, May 1994.
8. Z. Manna and A. Pnueli.The Temporal Logic of Reactive and Concurrent Systems:
Specication. Springer-Verlag - ISBN 0-387-97664-7, 1992.

Mechanized Analysis of Behavioral Conformance
in the Eiffel Base Libraries
Steffen Helke and Thomas Santen
Technische Universitat Berlin
Institut fur Kommunikations- und Softwaretechnik
FR 5-6, Franklinstrasse 28/29, D-10587 Berlin
email:[email protected], [email protected]
Abstract.We report on an analysis of the inheritance relationships in the Eiffel
Base Libraries, a library of container data structures. If inheritance is behaviorally
conforming, then polymorphism can be used safely, and the inheritance hierarchy
can be considered part of the interface of the library to its clients. We describe
a theory of object-oriented specication in higher-order logic that we used to
specify part of the Eiffel Base Libraries. With the theorem prover Isabelle/HOL,
we mechanically prove conformance relationships between those specications.
This work allows us to draw conclusions about the design of the Eiffel Base
Libraries, and about the feasibility of using an interactive theorem prover to apply
a strictly formal theory to the specication of a commercial product.
1 Introduction
One of the promises of object-oriented software development is to facilitate the reuse of
software components by incremental modication through inheritance, and by decou-
pling abstract interfaces from concrete implementations through polymorphism. Clients
commonly use the components of a library as they are provided. Therefore, the compo-
nents must have a precisely dened interface. An important piece of information that the
interface must make available to the clients are the inheritance relations in the library
that the clients may consider part of the interface. Only the inheritance relations of the
interface that yield a behaviorally conforming subclass allow clients to use polymor-
phismsafely. Therefore, it is worthwhile to study behavioral conformance in a library
of components designed for reuse, in particular for inheritance relations that the library
designers consider part of the library's interface. Unless clients are sure that abstract
classes provide abehaviorally conforminginterface to more concrete classes of the li-
brary, they will pick only a few concrete classes of the library and base their code on
the interfaces of those classes. Thus, their code will be more sensitive than necessary to
a change of the implementation of a data structure they use. On the other hand, if the
clients may trust in the conformance of the inheritance relations in a library, they can
design their software to rely on the interfaces to objects provided by abstract classes only.
The resulting code will be more abstract and robust to changes of the implementation of
objects.
Not all libraries of object-oriented components, however, consider inheritance re-
lations part of their interface to clients. TheLibrary of Efcient Data Structures and
J.N. Oliveira and P. Zave (Eds.): FME 2001, LNCS 2021, pp. 2042, 2001.
cSpringer-Verlag Berlin Heidelberg 2001

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries 21
Algorithms(LEDA) [11], for example, uses inheritance for implementation purposes
only. The inheritance hierarchy presented to clients basically is at. Cook [2] investi-
gated behavioral conformance (based on America's [1] notion of behavioral subtyping)
between the Smalltalk-80 collection classes. The conformance hierarchy that he derived
from the specications of those classes exhibits multiple relations between the classes.
Contrasting the conformance hierarchy with the inheritance hierarchy, he notes that the
two are mostly unrelated and in some cases even contradict each other.
In contrast to LEDA and the Smalltalk-80 library, a design goal of the Eiffel Base
Libraries [10] was to accomplish a Linnean reconstruction of the fundamental software
structures.:::to devise a coherent overall structure, in which every important variant
will have a precise place deduced from the application of a small number of classication
criteria [10]. Therefore, the rich inheritance hierarchy in the Eiffel Base Libraries must
be considered part of the interface of the libraries. It is designed to provide various
abstractions (or views) of the objects that implement concrete data structures.
Using a theory of object-oriented specication that we have developed with the
theorem prover Isabelle/HOL, we have investigated the conformance relations part in
the Eiffel Base Libraries. The aim of this work was to provide mechanized tool support
for reasoning about software components and to test the feasibility of such an approach
on a practically used software product.
In Section 2, we give a brief overview of the part of the Eiffel Base Libraries that
we worked on. Section 3 discusses why specifying classes is useful and introduces our
specication notation. The representation of specications in Isabelle/HOL is the topic
of Section 4. Section 5 introduces behavioral conformance and the way we have dened
it in higher-order logic. We analyze the way classes are built by inheritance in the Eiffel
Base Libraries in Section 6. Section 7 shows how those constructions can be mimicked
at the specication level. Section 8 summarizes the work on the specications with
Isabelle. We conclude in Section 9 with observations about the Eiffel Base Libraries as
a software product and with an analysis of our work with Isabelle/HOL.
2 The Eiffel Base Libraries
The several hundred classes of the Eiffel Base Libraries are grouped into ve main
libraries: thekernel,data structure,iteration,Lex, andParselibraries. We concentrate
on the data structure library. It is the largest part of the Eiffel Base Libraries and covers
fundamental data structures and algorithms, such as lists, arrays, queues, stacks, trees,
and hash tables. Because we investigate the data structure library only, we use the name
Eiffel Base Libraries as a synonym for the data structure library in the following.
The data structures covered by the Eiffel Base Libraries are container structures:
their objects are collections of items that may be changed and accessed according to
the specic properties of the data structure. Figure 1 shows the part of the Eiffel Base
Libraries on which we focus our investigation. The root of the class hierarchy of the
data structure library is the classCONTAINERshown in Figure 2. Because the typeG
of the items is irrelevant for a container, the classes of theCONTAINERhierarchy are
generic inG. The interface of the classCONTAINERcontains three basic features that
any container structure must provide: the testhas(v)determines if the container object

22 S. Helke and T. Santen
CONTAINER
COLLECTION TRAVERSABLE BOX
LINEARBAGSET HIERARCHICAL FINITE
BILINEARACTIVETABLE UNBOUNDED BOUNDED
CURSOR_
STRUCTURE
SEQUENCEINDEXABLE
CHAIN
DYNAMIC_
CHAIN
LIST
DYNAMIC_LIST
LIST
LINKED_
Fig. 1.TheCONTAINERhierarchy.
contains an itemv; the attributeemptyis true if the container does not contain any item;
the attributelinearrepresentationprovides access to the container as a sequence (of
typeLINEAR[G]).
The keywordsrequireandensureare part of the assertion language of Eiffel that
makes it possible to state preconditions (require) and postconditions (ensure) of features,
and class invariants, and check their validity during execution of an Eiffel program. We
will discuss the assertion language in more detail when we consider specications of
Eiffel classes in Section 3.
A major design principle of the Eiffel Base Libraries is to organize the inheritance
hierarchy according to a taxonomy of container structures. The three direct descendants
ofCONTAINERrepresent three criteria groups of related properties that serve to
describe containers.
Theaccesscriterion describes how the clients of a container can access its items.
For example, only the top item of a stack is accessible to its clients, whereas the
clients of an array can access each of the items of the array by an index. The class
COLLECTIONis the root of the access hierarchy.
Thetraversalcriterion describes how the clients of a container can navigate through
the container, accessing each of its items in turn. For example, a particular kind
of list may allow traversals only from the front to the back of the list, whereas
another kind of list may also allow to traverse it from the back to the front. The class
TRAVERSABLEis the root of the traversal hierarchy.
Thestoragecriterion describes the cardinality of a container and the ways to change
the cardinality. For example, some containers are nite, others are potentially innite.
A nite container may have a xed size, or its size may be unbounded. The class
BOXis the root of the storage hierarchy.

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries 23
classCONTAINER[G]
featurehas(v:G):BOOLEANis
deferred
ensurenotfoundinempty:Resultimplies notempty
end;
featureempty:BOOLEANis
deferred
end;
featurelinearrepresentation:LINEAR[G]is
deferred
end;
featureobjectcomparison:BOOLEAN
.
.
.
end
classCOLLECTION[G]
inheritCONTAINER[G]
featureextendible:BOOLEANis
deferred
end;
featureprunable:BOOLEANis
deferred
end;
featureput;extend(v:G)is
requireextendible:extendible
deferred
ensureiteminserted:has(v)
end;
featurell(other:CONTAINER[G])is
do :::
end;
featureprune(v:G)is
requireprunable:prunable
deferred
end;
featureprune
all(v:G)is
requireprunable:prunable
do ::: ensureno
moreoccurrences:nothas(v)
end;
featurewipeoutis
requireprunable
deferred ensurewiped
out:empty
end;
end
classBAG[G]
inheritCOLLECTION[G]
redeneextend
end
featureoccurrences(v:G):INTEGERis
deferred ensurenot
negativeoccurrences:Result>=0
end;
featureextend(v:G)is
deferred ensure thenone
moreoccurrence:occurrences(v)=old(occurrences(v))+1
end
Fig. 2.Container classes.

24 S. Helke and T. Santen
classACTIVE[G]
inheritBAG[G]
featureitem:Gis
requirereadable:readable
deferred
end;
featurereadable:BOOLEANis
deferred
end;
featurewritable:BOOLEANis
deferred
end;
featurereplace(v:G)is
requirewritable:writable
deferred
ensureitemreplaced:item=v
end;
featureremoveis
requireprunable:prunable;
writable:writable
deferred
end;
invariant
writableconstraint:writableimpliesreadable;
emptyconstraint:emptyimplies(notreadable)and(notwritable)
end
Fig. 3.Active containers.
Each class in theCONTAINERhierarchy provides a view to containers with a par-
ticular combination of properties. The (deferred) classes near the root of the hierarchy
provide very abstract views of containers. For example the classBAGshown in Fig-
ure 2 adds only one feature to the ones it inherits fromCOLLECTION: the feature
occurrence(v)returns the number of occurrences of the itemvin the container. Thus,
the classBAGimplicitly represents the property that a bag may store an item more than
once. The leaves of the container hierarchy, such asLINKED
LISTat the bottom of
Figure 1, are effective classes implementing a specic kind of container structure.
The siblings that directly inherit from the same class in some cases represent alter-
native properties of the class of containers their parent class represents. For example, the classesSETandBAGrepresent such a choice point. The featureoccurrence(v)
provided byBAGis useless for sets, because a set may contain an itemvat most once.
The classSETdeclares an attributecount, instead, that holds the number of (different)
elements in a set. It also strengthens the postcondition of the featureprune(v), which it
inherits fromCOLLECTION(c.f. Figure 2). The featureprune(v)removes an occurrence
ofvfrom the container. For a set, which may containvat most once,prune(v)removesall
occurrences ofv, i.e. it ensuresnothas(v). For a bag, in contrast,prune
all(v)establishes
that postcondition, butprune(v)does not necessarily do so.
Other branches in the inheritance hierarchy represent independent properties, which
may be combined further down in the hierarchy by multiple inheritance. For example, the descendantTABLEofBAGdescribes containers whose items are accessible through
keys. Figure 3 shows the classACTIVE, which is another descendant ofBAG. The class
ACTIVEdescribes containers that have a (possibly undened) current item (called
item) on which access and modication features work. Being accessible through keys
and having a current item are not contradictory properties of a container. The class CHAIN, which is a common abstraction of (non-circular) lists and circular containers,
combines those properties by multiple inheritance. Thus, the interfaces ofTABLEand
ACTIVEboth provide valid views of a chain.

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries 25
Collection[G]
ST A T E
c: bagG
visible
empty:Bool
extendible:Bool
prunable:Bool
linrep: seqG
empty=true,c=
prunable=true)empty=false
items linrep=c
ll
(c;empty;extendible;prunable;linrep)
other?:Collection[G]
c
0
=c]items(other?:linrep)
INIT
c=
has
v?:G
result!:Bool
result!=true,v?c
extend
(c;empty;extendible;
prunable;linrep)
v?:G
extendible=true
v?c
0
fv?gc=fv?gc
0
pruneall
(c;empty;extendible;prunable;linrep)
v?:G
prunable=true
v?c)c
0
=fv?gc
:v?c)(c
0
=c^empty
0
=empty^
extendible
0
=extendible^
prunable
0
=prunable^
lin
rep=linrep
0
)
prune
(c;empty;extendible;prunable;linrep)
v?:G
fv?gc
0
=fv?gc
c]v?=1)c
0
=c
c]v?>1)c
0
]v?<c]v?
Fig. 4.Specication ofCOLLECTION.
3 Specication of Library Classes
Eiffel is one of the few programming languages that supportassertions. Assertions are
Boolean expressions that are evaluated at run-time (if the program is compiled with the
appropriate compiler option). An assertion that evaluates tofalseraises an exception.
Assertions thus provide a valuable tool for debugging programs.
The assertion language is similar to an algebraic specication language that allows
one to specify relations between the functions (i.e. the features) of a given signature
(i.e. a class). Nevertheless, assertions are too weak to state all relevant properties of
a class. In particular for abstract deferred classes, it often is impossible to state
assertions that describe the intended functionality of a feature. For example, there are no
assertions about the attributeemptyofCONTAINER(c.f. Figure 2), because the features
available inCONTAINERare not expressive enough to state a postcondition onempty
that captures the intended meaning of that attribute.
1
Similarly, there are no constraints
on the attributelinear
representationofCONTAINER, because it is impossible to state
that the items inlinearrepresentationare exactly the items in the container object.
1
The characterization ofemptyby8v:G:has(v)cannot be coded by assertions, because
it is impossible to quantify over all elements ofGin an assertion

26 S. Helke and T. Santen
We use a notation similar
2
to Object-Z [17] to specify the intended behavior of classes
in a model-based way. Refering to a (hidden) mathematical model of containers, we
can easily express the effect of features on a container. Figure 4 shows the specication
of the classCOLLECTION, whose Eiffel code is sketched in Figure 2. The semantics
of our notation is given by representing it in higher-order logic a topic that we address
in Section 4.
A collection is a mutable container structure storing a number of items of a setG.
It can be tested whether a collection is empty and whether it contains a given item. A
collection can be extended by a single item (extend) or the items of another collection
(ll). Conversely, duplicate items can be removed from a collection, but once an item
with a particular value has been added to the collection, at least one item with an equal
value must remain in the collection. The attributelin
repgives access to a representation
of the collection as a sequence.
The constituents of the class specication are gathered in aclass schemacalledCol-
lection[G]. The parameter indicates that the class is generic in a setGof items. The rst
component of the class schema is the state schemaS
TATE. It describes the valid states of
the objects of the class, including attributes of the objects that are observable by other objects. The rst componentcof the state is the mathematical model of a collection, a
bag.
Bags are dened relationally by partial functions from the set of itemsGto the
positive natural numbers,bagG==G
1. Bags are formed using double brackets,
v
1;:::;v nfor itemsv 1;:::;v n, the membership test for bags isvc,b]dis the
union of two bags, andb]vis the number ofv's inb. The functionitemsmaps sequences
to bags. The domain anti-restrictionDRrestricts the domain of relationRto items
not inD.
In contrast toc, which is not accessible from outside of the class, the state components
below the keywordvisibleare externally visible attributes. Visible state components are
a notational abbreviation for methods returning values that depend only on the internal state of an object, so-calledobserver methods. The predicate below the horizontal line
of the state schema is thestate invariant. It describes the relationship between the state
components of valid objects.
The schemaI
NITdescribes the valid initial states of objects: the containercis initially
empty, and, because the state invariant is implicitly required byI
NIT,empty=trueand
lin
rep=hi.
The schemashas,extend,ll,prune, andpruneallspecify the methods of the class.
Like in Object-Z, input and output variables are decorated with question marks and exclamation marks, respectively. Undecorated variables refer to the state of the object before executing the method (pre-state), primed variables to the state after executing the
method (post-state). The method schemas of a classimplicitlyrefer to the state schema,
and the notation(x;y;z)is used to indicate that the method may change only the state
componentsx,y, andz.
The observation that the assertions of a class are insufcient to specify the intended
behavior of its objects properly is also valid for the classes further down in the container
2
The history constraints we use are not part of Object-Z, and we do not support all language
features of Object-Z

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries 27
ACTIVE[G]
BAG[G]
ST A T E
visible
item:G
readable:Bool
writable:Bool
readable=true)item c
empty=true)(readable=false^writable=false)
writable=true)readable=true
replace
(c;item;readable;writable;linearrepresentation)
v?:G
writable=true
item=v?)c
0
=c
item6=v?)count(c
0
)=count(c)fitem7!(c(item)1)g
fv?7!(c]v?+1)g
item
0
=v?
remove
(item;c;readable;writable;extendible;prunable;linearrepresentation;empty)
prunable=true
writable=true
count(c
0
)=count(c)fitem7!(c(item)1)g
Fig. 5.Specication ofACTIVE.
hierarchy, which have a richer structure. The assertions of the classACTIVE(c.f. Figure
3), for example, do not at all clarify the purpose of the new features it declares. The
postcondition ofreplace(v), which shall replace the parametervfor the current item of
the container, ensures that the attributeitemequalsv, but it cannot state the effect of
replace(v)on the container. The method could just set the attribute that holds the value
of the current item tov, and leave the container data untouched.
The specication ofACTIVEin Figure 5, in contrast, claries the effect ofreplace(v)
on the internal data of the container, which, for this class, is a bagc: bagG. It relates
the value ofitemto the elements ofcand requirescto change accordingly. The function
count(c)maps a bagcto a total function of the same type that maps all items not in the
domain ofcto0.
The preceding examples do not question the use of assertions as a documentation of
Eiffel code and as a tool for effective debugging, but they show that specications in a
more powerful language than the assertion language of Eiffel can extend the informa-
tion provided by assertions to include information about the intended functionality of
features. That information is not only useful as a documentation for users of the Eiffel
Base Libraries, but it also is indispensable for a machine assisted analysis of the library.

28 S. Helke and T. Santen
4 Representation of Class Specications in Isabelle/HOL
Since our aim is to come up with tool support for reasoning about class specications, we
must map the Object-Z-like specications of classes to a logical formalism for which a
proof tool exists. To this end, we use Isabelle/HOL, the implementation of higher-order
logic (HOL) in the generic theorem prover Isabelle [12]. Our representation of class
specications builds on the representationHOL-Z[8] of plain Z in Isabelle/HOL, which
we extend by denitions of object-oriented concepts.We have derived an extensive theory
about those concepts using Isabelle, and we have implemented a number of tailor-made
proof procedures that provide efcient proof support to work with concrete specications
such as the ones describing the Eiffel Base Libraries.
In the following, we can only very briey introduce the general approach of repre-
senting class specications in HOL and reasoning about them using Isabelle. For a more
detailed description of the theory and its implementation, we refer to [8,13].HOL-Z
and the complete theory of object-oriented specication in HOL are described in [16].
4.1 The Type of Classes
InHOL-Z, the schemas of Z are represented by predicates in HOL, i.e. a schema
denition of Z is mapped to a function denition in HOL. The dened function maps
the tuple of the signature components of the schema to the Boolean values (in HOL, the
truth values are just ordinary values). This leads to a so-called shallow embedding of
Z in HOL, where the expressions of Z are considered as a concrete syntax for certain
expression of HOL. The strong similarity of the semantics of Z and HOL justies that
view [14].
To represent object-oriented specications, we extendHOL-Zby dening a type
of classes in HOL. For technical reasons, we distinguish between the constant and the
mutable part of the state of an object in that denition: Given thatis the type of method
identiers, the typesandare the types of the immutable and mutable parts of the
object state, and the methods of the class have the input typeand the output type!,
then the type(; ; ; ; !)Classconsists of all class specications whose components
have the respective types.
(; ; ; ; !)Class
typ
=f(C;S;I;Mths;H)j
(C::Const)
(S:: (; )State)
(I:: (; )Init)
(Mths:: (; ; ; ; !)Methods)
(H:: (; )History):
Cls
3
C S I Mths Hg
(1)
According to that type denition, a class specication is represented by a quintuple
(C;S;I;Mths;H). The componentsCandSare schemas describing invariants over the
constant and mutable part of the objects'state. The predicateIrepresents the initialization
schema. The method suiteMthsis a (nite) function mapping method identiers to
representations of operation schemas specifying the methods of the class. The predicate

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries 29
Collection G
def
=(basicclass(CollConst G)(CollState G)(CollInit G)(CollHist G))
(
00
empty
00
;empty G)
(
00
extendible
00
;extendible G)
(
00
prunable
00
;prunable G)
(
00
lin
rep
00
;linrep G)
(
00
has
00
;has G)
(
00
extend
00
;extend G)
(
00
prune
00
;prune G)
(
00
prune
all
00
;pruneall G)
(
00
ll
00
;ll G)
Fig. 6.Representation ofCOLLECTIONin Isabelle/HOL.
H, thehistory constraint, is a relation between before and after states of the objects of
the class.
Finally, the predicate(Cls
3
C S I Mths H)describes theinternal consistencyof the
class. It is dened by four conditions, which ensure that the constituents of a class refer
to each other in a way that conforms to our intuition of a class specication:
1. The constant of an object's state can be chosen independently of the mutable part
of its state.
2. The initialization establishes a state that satises the state invariant.
3. The history constraint relates only states satisfying the state invariant.
4. Each operation schema specifying a method of the class relates only states satisfying
the invariant, and it respects the history constraint.
Internal consistency establishes a semantic relation between the components of a
class that is in part indicated by the Object-Z-like notation we use to denote class speci-
cations (c.f. Figure 4). For example, it is understood that the methods of a class implicitly
refer to the properties of its state schema and constant declarations. The logical repre-
sentation, however, must make these conditions explicit, because much of the theory
about classes derived in Isabelle/HOL relies on them.
4.2 Class Constructors
The type denition(1)abstractly introduces the concept of a class in HOL. Thus, we
can dene HOL functions that construct class specications. Those functions take as
parameters the representations of Z schemas provided byHOL-Zof the component
specications of a class. For example, Figure 6 shows the representation of the speci-
cation ofCOLLECTIONgiven in Figure 4.
The functionbasicclassconstructs a class specication without methods, the func-
tionsandadd the specication of an observer or of an ordinary method to a class
specication. Thus, the denition ofCollection Gin Figure 6 rst builds a class without
methods from the schemas describing the invariant and the initialization of the class.
For example,(CollInit G)is the HOL predicate representingI
NITof Figure 4. Then,

30 S. Helke and T. Santen
the denition successively adds the specications of observers and the other methods of
COLLECTION, whereextend G, for example, is the representation of the schemaextend
of Figure 4. The string
00
extend
00
is the identier ofextend GinCollection G. We can use
it to select the method specication from the class specication, e.g. to model method
invocations. The setids(Collection G)is the set of method identiers ofCollection G.
To be able to work with a class specication in HOL, we must show that its com-
ponents are internally consistent, i.e. that they satisfy the predicateCls
3
. A tactic im-
plemented in Isabelle accomplishes that proof fully automatically for specications
adhering to the usual style of specifying in Z.
5 Behavioral Conformance
Polymorphic assignments in object-oriented languages allow us to express the substitu-
tion of (an object of) a data type for another in a program at the level of the programming
language. Thus, polymorphism is a means of the object-language to express the meta-
language substitution of programs for programs in the context of a client program. We
may therefore apply the concept of data type renement to answer the question whether a
variable can safely be bound to an object of a proper subtype of the variable's static type.
America [1] coined the termbehavioral subtyping
3
for this property. Using Hoare-triples
to specify the behavior of methods of an object type, he requires that the specication of
a subtypedata renesthe specication of a supertype (using a function from subtype to
supertype as the simulation relation). He uses the well-known forward simulation rule
of data renement with a retrieve function as it is commonly used for Z (see, e.g., [18]).
5.1 Extra Methods
Rephrased in object-oriented terminology, America's denition of behavioral subtyping
requires that no program can distinguish whether a particular variable is bound to an
object of its static type or to an object of a proper subtype of that type provided that
the program uses the interface of the supertype only. This restriction on the observing
programs is inadequate for most (imperative) object-oriented programming languages,
because it is common practice to access the same object via different interfaces.
If we allow sharing of object references in observing programs, we must take the
effect of the extra methods of a subtype into account in the denition of behavioral
subtyping. Theextra methodsof a subtype with respect to a supertype are the meth-
ods of the subtype that do not directly correspond to methods of the supertype. Liskov
and Wing [9] proposed two modications of America's denition of subtyping to ac-
count for extra methods. We use the relation between the classesCONTAINER[G]and
COLLECTION[G]shown in Figure 2 to illustrate Liskov and Wing's propositions. The
purpose ofCOLLECTION[G](and many other classes of the Eiffel Base Libraries) is
3
The term behavioral subtyping is misleading, because the logical relationship that America
[1] denes may hold between classes that are not related by inheritance. We call that relationship
behavioral conformancethroughout this paper. Only in the remainder of the present section,
where we refer to the terminology of others, will we stay with the term behavioral subtyping.

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries 31
to extendCONTAINER[G] by several new methods, leaving the inherited methods un-
touched. Even this small example shows that considering extra methods is indispensable
for reasoning about object-oriented component libraries.
Extension Rule.One approach to address subtyping in the presence of extra methods
is to interpret a class specication as a complete description of the possible behaviors
of all objects of the class including objects of subclasses. Liskov and Wing [9] call
that theextension ruleof subtyping. In this interpretation, the methods of a class induce
the behavior of its objects. All changes of an object's state are caused by the methods
dened by its class, and we can identify the objects of a class with the inductively dened
set of traces whose starting points are initial objects and which are extended by method
applications. Then, extra methods can but mimic the behavior that is already possible
without using extra methods.
Consider the relationship between the classesCONTAINERandCOLLECTION
shown in Figure 2. The classCONTAINERdenes the observershas,empty, andli-
near
representation, but it does not provide a method to change an object's state. The
classCOLLECTIONinherits fromCONTAINERand introduces new methods to add
items to a container and remove items from it.According to the extension rule,COLLEC-
TIONisnota behavioral subtype ofCONTAINER, because the mutatorsextend,prune,
etc. cannot be explained by the methods inherited fromCONTAINER(because the latter
are observers only).
Constraint Rule.The designers of the Eiffel Base Libraries clearly intended the class
CONTAINER, which is the root of the inheritance hierarchy of the libraries, to provide
the most abstract interface to any object of a container type. A descendant such as
COLLECTIONshould be accepted as a behavioral subtype ofCONTAINER, but the
principal assumption underlying the extension rule that the methods of a class induce all
possible behavior of its objects is obviously not satised for that inheritance hierarchy.
We must assume that the designers of the library have a more liberal view on subtyping:
the description ofCONTAINERdoes not forbid that objects change, therefore a subclass
may introduce mutators.
Theconstraint ruleof subtyping [9] reects this liberal view: any behavior of an ob-
ject is admissible unless the specication of its class explicitly disallows it. Liskov and
Wing augment class specications byhistory constraintsto restrict the admissible be-
havior of objects. History constraints are relations of object states describing admissible
state changes of objects independently of the changes that the methods make possible.
The constraint rule requires that the history constraint of a subclass is sufcient for the
one of the superclass. The rule poses the same restrictions on methods as America's
denition of subtyping, allowing for weakening of preconditions. Weakening the pre-
condition of a method does not lead to subtyping relations contradicting the intuition
that the history constraint describes the possible behaviors of an object, because Liskov
and Wing require all methods of a class to satisfy the history constraint. We captured
that requirement in the denition of internal consistency.

32 S. Helke and T. Santen
In the example of Figure 2, we assume an unconstrained history (the full relation on
valid states of objects) forCONTAINER. With that specication ofCONTAINER, the
constraint rule establishes thatCOLLECTIONis a behavioral subtype ofCONTAINER.
5.2 Behavioral Conformance in Isabelle/HOL
We have dened the analog of Liskov and Wing's constraint rule for our specications
in Isabelle/HOL. That denition is quite lengthy and its exact technical phrasing is not
important for this paper. In the following, we therefore paraphrase the denition in a
condensed form using Z schema calculus. For more details, we refer the reader to [16].
The predicateconformsdenes behavioral conformance in HOL. It is declared as
follows:
conforms:: [ (;(;
0
;!;!
0
)IOconv)nmap;(;
0
)nmap;(;
0
;;
0
)retrv;
(; ; ; ; !)Class;(
0
;
0
;
0
;
0
;!
0
)Class]!bool
For two class specicationsA=(AConst;AState;AInit;AMeth;AHist)andC=
(CConst;CState;CInit;CMeths;CHist), the propositionconformsRACis true if
Cbehaviorally conforms toAwith the retrieve relationR, the signature morphism,
and the conversionof input/output types between the methods ofAand the methods
ofC.
The relationRrelates the states ofAto the states ofC. Unlike America (and data
reication in VDM [6]) we do not requireRto be a function, because it turns out that
some conformance relationships in the Eiffel Base Libraries require that more liberal
view of data renement, which is also the usual one for Z [4,18].
The signature morphismmaps the names of the methods inAMethsto the names
of the methods inCMeths. For each method ofAit thus identies the method ofCthat
simulates it.
We need the type conversionfor technical reasons: HOL is strongly typed. There-
fore, we need to inject the different input and output types of the operation schemas
specifying the methods of a class into a common type that we can use asthetype of
inputs and outputs, respectively, of the method suite of the class. As a consequence
of that representation of classes, the input/output types of different classes, in general,
are different. To relate single methods of two classes, we need to map a subset of the
input/output type of one class to an isomorphic subset of the input/output type of the
other class. The conversionis a family of isomorphisms [15] (indexed by the method
identiers ofA) that accomplishes that task.
Paraphrased without the technical overhead we just discussed,conformsRAC
requires the following conditions to hold:
1. The signature morphismmaps all methods ofAto some ofC:
dom=ids A^ranids C
2. All concrete initial states represent abstract initial states:
8CConst;CStateCInit)9AConst;AStateAInit^R

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries 33
3. The preconditions of the abstract methods imply the preconditions of the concrete
methods:
8n:dom;AConst;AState;CConst;CState;inp n?:X n
preAMeths(n)^R)preCMeths((n))
4. The concrete methods simulate the abstract methods:
8n:dom;AConst;AState;CConst;CState;CState
0
;inpn?:X n;outn!:Yn
preAMeths(n)^R^CMeths((n)))9AState
0
R
0
^AMeths(n)
5. The concrete history is sufcient for the abstract history:
8CConst;CStateCHist)9AConst;AStateAHist^R^R
0
Those conditions are just the conditions of forward simulation rephrased to classes
and augmented with the constraint rule that handles extra methods.
5.3 Transitivity of Conformance
Our denition of behavioral conformance in HOL is strictly formal. Therefore, we
can derive properties of conformance mechanically within higher order logic using
Isabelle/HOL. One important property that we have derived in that way is the transi-
tivity of conformance: Given three classesA,B, andC, and conformance relationships
betweenAandB, andBandC, we know thatCalso conforms toA:
conforms ababRabA B conforms bcbcRbcBC ac=:::
conforms ac(ab mbc)(RablRbc)AC
(2)
6 Inheritance in the Eiffel Base Libraries
In the following, we identify patterns of inheritance in the Eiffel Base Libraries. Each of the patterns corresponds to an operation that constructs a class schema from another one. Those specication building operations do not necessarily produce a behaviorally conforming subclass of their parameter class. Therefore, it would be inadequate to call one of them the inheritance operation of our specication language.
There are ve ways the classes in the hierarchy
4
of Figure 1 are constructed by
inheritance, none of which, in general, yield behaviorally conforming subclasses:
1.add new methods: extend the parent by new extra methods;
2.redene methods: change the specication or implementation of methods inherited
from the parent class;
4
This hierarchy includes just the inheritance relations that we consider part of the interface of
the Eiffel Base Libraries; the gure does not show inheritance that is used for implementation
purposes only.

34 S. Helke and T. Santen
3.add new attributes: extend the parent by new attributes, thus extending the state of
the object;
4.hide a feature: export the feature toNONE, thus excluding it from the interface of
the new class;
5.combine classes by multiple inheritance: combine several classes into one, selecting
a denition from one class for each feature whose name appears in several of the
inherited classes.
Most inheritance relations of the container hierarchy are combinations of those inher-
itance patterns. For example, the classBAG(c.f. Figure 2) extendsCOLLECTIONby
the new attributeoccurrences, and it redenes the methodextend.
We use the following specication building operations to construct specications
according the inheritance patterns: The constructorof class schemas (c.f. Section
4.2) extends a class schema by a new method. We can also use it to model redenition,
because ifn2ids Cls, thenCls(n;OP)overrides the denition ofninCls.
Introducing new attributes involves two modications of the specication: rst, it
modies the state schema to include the new attribute and describe its invariant relations
to the other state components; second, it adds a new observer method to the class schema.
Modifying the state schema to include a new attribute is a special case of changing the
internal model of a class schema such that, under certain conditions, the resulting class
schema behaviorally conforms to the original one. We dene an operation on class
schemas to change the internal model of a class schema and characterize the conditions
under which it yields a behaviorally conforming subclass in the following Section 7.
7 Subclass Calculation
Just as it is much more productive to build subclasses from classes by inheritance in
Eiffel, it is necessary to construct specications of subclasses from the specications
of their superclasses. It would be infeasable to specify each class in the Eiffel Base
Libraries from scratch, because the resulting specications would become very large
and incomprehensible.
In the preceeding section, we showed that most of the constructions in the Eiffel
Base Libraries can be mimicked on the specication level with the class constructors of
Section 4. In this section, we dene another class constructor, thesubclass calculator,
that allows us to change the mathematical model of a container when constructing the
specication from a subclass from the specication of a class. Under certain conditions,
the resulting specication behaviorally conforms to the original one.
7.1 The Subclass Calculator
The subclass calculator works dually to a posit-and-prove approach to behavioral con-
formance. Instead of dening two classes schemas and exhibiting a retrieve relation to
establish behavioral conformance, the subclass calculator maps a class schema and a
retrieve relation to a new class schema. The calculator uses the conditions of behavioral
conformance to specify the components of the resulting concrete class in terms of the

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries 35
given abstract class and the retrieve relation. Roughly, the calculator conjoins the com-
ponents of the abstract class with the retrieve relation, and existentially quanties over
the abstract constants and states in the resulting formula. The construction for methods
relies on the the data renement calculator that Josephs [7] denes to construct a
concrete operation schema as a data renement of an abstract one in Z.
In HOL, the functionSimBymaps a given class and a retrieve relation to a new class.
SimBy:: [ (; ; ; ; !)Class;(;
0
;;
0
)retrv]!(;
0
;
0
;;!)Class
The components ofSimBy Cls Rare dened as follows:
The constant and state schemas of the calculated subclass are dened in terms of
the conjunction of the constant and state schemas ofClsand the retrieve relationR,
and hiding the abstract entities.
For each methodMofCls, there is a methodM
0
of the calculated subclass. The
precondition ofM
0
contains all pairs of constants and states for which abstract
constants and states exist that satisfy the precondition ofM. For those states, the
concrete operation relates the pre- and post-states for which abstract ones exist that
satisfyM.
M
0def
=(9cs:preM c s inp^Rcccscs)^
(8cs:preM c s inp^Rcccscs)
(9s
0
:R c cc s
0
cs
0
^Mcss
0
inp out)))
The history schema of the calculated subclass is dened similarly to the constant
and state schemas. The retrieve relationRestablishes correspondences between the
abstract and the concrete pre- and post-states.
Josephs [7] already notes that the data renement calculator for Z does not always
yield a renement. For general retrieve relationsR, it is still necessary to check the
applicability condition relating the preconditions of abstract and concrete operations.
(c.f. Section 5.2). If, however, the retrieve relationRis a function from the concrete onto
the abstract states, then the calculated subclassSimBy Cls Rbehaviorally conforms to
Cls. That condition onRcorresponds to the adequacy condition of data reication in
VDM [6], which admits functional abstractions only. The predicateis
surjfundenes
that condition formally.
is
surjfun R(cma Cls)(sma Cls)CVs=IdentList
io

=
Cls M=id m(ids Cls)
conforms CVs M R Cls(SimBy Cls R)
(3)
Theorem (3) is of great practical importance. It establishes once and for all the
relatively simple conditions under which subclass calculation implies behavioral conformance. As the next section will show, subclass calculation is suitable to dene the specications of most classes of the Eiffel Base Libraries. Theorem (3) helps a lot to simplify proofs of behavioral conformance between those specications compared to proofs against the denition of behavioral conformance. In particular, the theorem does not require the proof to consider the method suites of the two classes, which otherwise is the major work in a proof of behavioral conformance.

36 S. Helke and T. Santen
7.2 An Alternative Representation ofCollection
Using the subclass calculator, we can build a specication ofCollectionfrom the spec-
ication ofContainer. The internal model ofContaineris a set of the items in the
container. The internal model we use inCollection, however, is a bag (c.f. Figure 4).
Given a relationR
Cont
Coll
that equates the internal model ofContainerto the domain ofcin
Collection, we can construct the specication ofCollectionby calculating a subclass of
Containeraccording toR
Cont
Coll
and augmenting the resulting class with the extra methods
ofCollection:
Collection G
def
=(SimBy(Container G)R
Cont
Coll
)
(
00
prunable
00
;Prunable G)
:::(
00
prune
all
00
;Pruneall G)
We used that way of constructing specications to economically specify the classes
of the Eiffel Base Libraries shown in Figure 1.
8 Conformance Analysis of the Eiffel Base Libraries
We followed a ve step procedure to specify classes and analyze behavioral conformance
with Isabelle/HOL (see [5] for the technical details):
1. Specify a class in Object-Z-like notation; represent the specication as a class
schema in HOL. For the representation, decide whether to construct the class schema
independently of other class schemas, or to use the subclass calculator to construct
the class schema from another one. In the latter case, determine an appropriate
retrieve relation.
2. Prove the internal consistency of the new class schema, and derive unconditional
equations to select the components of the class schema.
3. Derive the preconditions of the methods of the new class schema.
4. Determine retrieve relations between the new class schema and the specications of
the immediate ancestors of the class in the inheritance hierarchy, if such relations
exist. Analyze whether or not the retrieve relations are surjective functions.
5. Prove behavioral conformance of the new class with its immediate ancestors.
Step 2 is strictly necessary to be able to prove non-trivial propositions about the
specic class schema. Deriving the preconditions in Step 3, however, mainly served to
validate the specications, because the retrieve relations we considered all were surjec-
tive functions such that we could apply Theorem (3) to prove behavioral conformance
in Step 5. If a class schema is constructed by subclass calculation in Step 1, then Step 4
only needs to analyze the function property of the relation used in Step 1.
Figure 7 shows the subgraph of theCONTAINERhierarchy that we considered. We
represented the classes in HOL that are shaded gray in the gure. The class schemas
of theCOLLECTIONandTRAVERSABLEhierarchies are dened in terms of their im-
mediate ancestors in those hierarchies. The class schemaBAGis a simple extension of

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries 37
INDEXABLE
TABLE
FINITE
BOX
CHAIN
specified class
coded in HOL and
internally consistent
conformance proved
CURSOR_
STRUCTURE
SEQUENCE
ACTIVE
preconditions derived
COLLECTION TRAVERSABLE
BILINEAR
LINEARBAG
CONTAINER
Fig. 7.The specied and analyzed subgraph of theCONTAINERhierarchy.
COLLECTIONby new methods (using). All other constructions in the two hierar-
chies are subclass calculations that are extended by new methods and observers for new
attributes. The transitions fromCONTAINERtoCOLLECTIONand toTRAVERSABLE
involve changes of the mathematical model of the container: inCONTAINER, it is a set,
whereas it is a bag inCOLLECTIONand a sequence inTRAVERSABLE. The construc-
tions of the other classes only extend the state with new attributes. The retrieve relations
for those constructions are therefore projections from the extended concrete state to the
abstract state.
To derive the internal consistency (Step 2) of the class schemas shaded gray in the
gure, we used a tailor-made tactic (c.f. Section 4.2). Deriving the preconditions (Step 3)
of the methods of all classes exceptCURSOR
STRUCTUREandSEQUENCE, served
to validate the specications. To derive the preconditions, we used a tactic to apply the one-point-rule in a sophisticated way, which included handling subclass calculations.All retrieve relations used in the subclass calculations, and also the one used to analyze the inheritance ofACTIVEbySEQUENCE, are surjective functions (Step 4). This allowed
us to rely on Theorem (3) when proving behavioral conformance relations (Step 5).
To achieve a high degree of automation, we implemented two tactics to prove con-
formance for the typical construction used in the library. Given an abstract class schema AClsthat construction consists of two steps: rst, we dened an intermediate class
schema
BCls=SimBy ACls R
by subclass calculation; second, we extended the class schemaBClsby a number of
methods (possibly overriding method denitions ofACls):
CCls=BCls(n
1;Op1):::(n k;Opk)
Our tactics consider conformance proofs for subclass calculation and extension by meth- ods, respectively. They automatically synthesize appropriate I/O conversions and handle

38 S. Helke and T. Santen
all proof obligations related to class schema constructions. Using the theorems about
subclass calculation of Section 7 and similar theorems about extension of a class schema
by a method, they reduce a conformance proposition to verication conditions on (the
HOL-Zrepresentations of) the Z schemas that make up the specication of the class.
They present only those verication conditions to the user of Isabelle to prove them inter-
actively. Thus, the two tactics establish behavioral conformance ofBClstoACls, and of
CClstoBCls. An application of Theorem (2), the transitivity of behavioral conformance,
completes the proof of conformance ofCClstoACls.
9 Conclusions
We conclude with an evaluation of our work on the Eiffel Base Libraries. First, we
discuss our experience with the libraries and their specication.. Then we draw some
conclusions about the suitability of our framework for applying it to the libraries.
The Eiffel Base Libraries.Setting up the specications of classes of the library and an-
alyzing their relationships required a detailed examination of their informal description,
their specication by assertions, and their implementation code, too. Often, Meyer's [10]
informal description of the purpose of classes and their features helped to clarify their
functionality, but occasionally it was necessary to inspect the code not only of the class
in question but also of its descendants, in particular the effective ones at the leaves of
the inheritance hierarchy, to determine the precise function of a feature in a class. This
was especially necessary to distinguish between similar features, such asextend,put,
andreplace,orpruneandremove.
Class specications concisely describe the possible behavior of objects.The resulting
specications capture not only the information that is directly present in the class de-
scription (by assertions and code), which is quite sparse for the deferred classes near the
root of the class hierarchy. Capturing information about the descendants of a class, too,
the specications describe the possible evolution of features (by late binding) when
moving down in the inheritance hierarchy toward effective classes. Thus, the specica-
tions disambiguate the functionality of features and describe in a single specication
not just a single class but the cluster of classes that inherit from that class. A class spec-
ication concisely captures the possible behavior of the objects of a class. Behaviorally
conforming subclasses assumed, the specication of a method completely describes the
possible effects of an invocation of the method at the presence of late binding and poly-
morphism. It is not necessary to inspect the different implementations of the method in
the descendants of the class.
Inheritance induces behavioral conformance.All inheritance relations in the part of the
libraries that we analyzed induce behavioral conformance. Therefore, it is safe to use
objects of those classes polymorphically, accessing them through an abstract interface,
as it is provided by the deferred classes in the library. This justies to consider the entire
inheritance graph shown in Figure 7, not just the interfaces of the classes, as part of the
interface of the Eiffel Base Libraries to their clients.

Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries 39
Table 1.Analysis of Class Specications.
Class Number of methods Proof time (in min.)
new total Internal Precondition
consistency analysis
CONTAINER 33 2 1
COLLECTION 811 17 10
BAG 212 2 4
ACTIVE 517 13 41
CURSORSTRUCTURE11 28 125
TRAVERSABLE 36 3 5
LINEAR 814 20 50
BILINEAR 216 10 25
SEQUENCE 14 30 130
Performance measured on a SUN-Enterprise 3000
with4UltraSparc-I processors (167MHz) and4GB main memory.
Retrieve relations are simple.The retrieve relations that relate immediate descendants to
their ancestors are relatively simple. Overriding the specications of inherited methods
is rarely necessary. These observations indicate that the individual classes encapsulate
few well-dened properties or design decisions rather than merging many in one
class.
Partial conformance can describe the effect of hiding methods.The inheritance relations
that are part of the interface of the libraries to clients are designed to ensure behavioral
conformance. Hiding features avoids duplicating classes in some places. In a strict sense,
hiding destroys conformance, because the signature morphism from the abstract to the
concrete class is necessarily partial. But, as Frick et. al. [3] observe, considering all
methods of a class often is unnecessary to ensure safe polymorphic uses: the conditions
of behavioral conformance need only hold for the methods that a context actually uses.
It is, of course, easy to dene a weaker notion of conformance in our framework that
does not require the signature morphism to be total.
The Framework.Table 1 gives an impression of the size and complexity of the appli-
cation of our tactics to the classes of Figure 7. It provides data on the sizes of the classes
and on the performance of the tactics establishing internal consistency and deriving pre-
conditions. The rst two columns show the number of methods that are newly dened
in a class and the total number of methods including the ones inherited from its parent
class (by a subclass calculation). It is common for a class to extend its parent class with
approximately ten new methods.
New methods determine the effort of internal consistency and precondition analysis.
The third column shows performance gures for proving the class schemas internally

Random documents with unrelated
content Scribd suggests to you:

[586] Näistä sanoista on moniat ollut niin pois-kuluneet, ettei heitä
ouk tainut lukea ykskään.
[587] Mitä näistä vapa-merkkilöistä tuloo sanottavaksi, niin suuri
osa heistä on niin vanhat, ettei heitä eneän tunnetak, liioitenkin
koska monet heistä on tainneet jo sammua ennen vuotta 1625,
jollon se Ruohtalainen Vapa-Huone, kuhun heitä sisään-kirjutettiin,
asetettiin; monet ovat myös muustakin syystä jäänneet siihen ylös-
panematak, alinomattain koska suurin osa meijän vanhoista
Suomalaisista vapasuvullisista, eivät kuulleet Ruohtalaiseen Vapa-
Huoneesen, mutta oli yksi peru niistä muinoisista Saksalaisista ja
Virolaisista Tempel-Herroloista, joihen vapaallisus oli Saksan maissa
perustettu. Kuin tähän vielä luetaan että näissä vapa-merkkilöissä
harvoin selitetään muuta kuin ainoastaan kilpeä, joka monessa oli
pian yhölläinen, ja jotka ainoastaan eroitettiin Rauta-kyperästä,
Sarviloista, tahi Kyperä-vaipasta (Hjelmtäcket), ja ettei heissäkään
painia paljon eroitetak, niin löyetään miten vaikkia se on näitä
selittää, liioitenkin koska usseen pois-vaihtelivat välillensä
vapamerkkilöitänsä, ja kantoivat vieraita äkkinäisiä, tahi muuten
muuttelivat omiansa.
[588] Minä olen kyllä kirjuttanut moneen paikkaan, tätä
kuulustellaksein, mutta en ouk soanut vastausta, joka toistaa miten
kylmäkiskoiset meijän moa-miehet vielä ovat näissä töissä.
[589] Brenner ei kirjuta tästä kivestä mitään muuta, kuin
ainoastaan nämät sanat: "I Åbo D. Kyrka."
[590] Hauta-varjo, Grafwård; Hauta-kivi, Grafsten.
[591] Peä-Kirkko (tahi Tuomio-Kirkko), Dom-Kyrka.

[592] Tässä jääpi yksi sana, välissä, toimittamak.
[593] Mutta tässä tarkoituksessa kahomme toas ouoksi, ja
varomme olevan uskottomattoman, että tämä kivi oisi muka ollut se
ainoa Turun kirkossa, joka vielä v. 1671 oisi ollut jälellä näistä
vanhoista ajoista; ja jota niin muoton oisi yksinään jäänyt
murentumatak näissä kauheissa Turun kirkon tuli-paloissa, jotka
tapahtui v. 1318, 1429, 1458 (1464, 1473?) 1546 ja 1656, kussa
kaikki muut kirkon kaunistukset — joit' eivät Juuttilaiset v. 1509, ja
Venäläiset v. 1318 hävittänneet tahi vienneet myötensä — paloi
tuhkaksi. Mutta kysytään siitten, tokkos Turun kirkko on niin vanha,
tahi oliko se jo 1248:nen vuuen tienoilla rakettu? Sitä emme saata
sanoa, ainoasti että v. 1229 peätettiin jo että muuttoo pois kirkko
Rantamäeltä (kussa Brenner niinikkään vielä v. 1671 tapais yhen
vanhan hautakiven vuotesta 1291? — kaho X Taul. kuv. 1) Turkuun,
eli niin kuin sitä muinon kuhuttiin Unikankareesen. Millonka tätä
tehtiin ei varsin tunnetak, mutta 1258:nen vuuen teinoilla jo
mainitaan tästä uuesta Turun kirkosta (Porth. Chr. p. 193). Jos sen
eistä tämä Turun pappi oisi ollut naitu ennen v. 1248, niin se oisi
vielä saattanut eleä monta myöhempänä. Toiseksi niin nämät
kirjoitus-nenät eivät teoltakaan näyk olevan niin vanhan-aikuiset, jos
heitä verroitetaan siihen toiseen kiven-kirjoitukseen joka löytyi
Rantamäellä.
[594] Yksi nimellinen Niiles Antinpoika oli v. 1303 Praefectus
Finlandiae (Peämies Suomessa) mutta se on mahotoin, että näillä
sanoilla tarkoitetaan häntä.
[595] Kunta, Sällskap, Orden, Gille, Veli-kunta t. Veljellisyys
Brödraskap, Papillinen Veli-kunta, ett Presterligt Gille.
[596] Kirkko-Tarinamus, Kyrko-Historie.

[597] Muistettava on myös, että jos tämä vapa-merkki kahottaisiin
kohallansa (niin kuin heitä aina kahotaan) niin silloin kirjutos alkaisi
ala-peästä kivee (jota en muualla ouk nähnyt); ja jos toas kivee
asetettaisiin kirjutoksensa mukaan, niin silloin toas vapamerkki
keäntyisi ylös-alaisin (joka oisi vielä sopimattomampi). Se näyttäis
ehkä silloin, kuin sillä kuvaeltaisiin yhtä Piispaan kypärätä (en
Biskopsmössa).
[598] Että tämä suku on vanha, arvataan siitä, että ne Ruotsin
muinoiset Kuninkaat Sverker den Gamle (joka kuoli 1155) jonka isä
Erik Årsäll oli vanhuuellansa ottanut Ristin uskoa, ja kasteessa
kuhtunut ihtesek Kol t. Koarle — kuin myös hänen poikansa Koarle
Sverkersson (joka kuoli 1168) ja toas hänen poikansa Sverker den
Unge (joka kuoli 1210) — sanotaan kaikki olleen tästä Natt och
Dagin suvusta, ehkeivät kantaneet tätä suku-nimee, joka otettiin
tavaksi vasta myöhöisämpinnä aikoina. K. Vapa-Huoneen polvi-
laskuissa, alotetaan tämä suku vasta v. 1220 yhestä Pentti
Matinpojasta, joka oli ollut Kuninkaan Eerikki Läspin Valta-Neuo.
[599] Tämä (nykyinen) Natt och Dagin suku tuli v. 1625
Ruohtalaiseen Vapa-Huoneesehen sisään-otetuksi 13:nen N:on alla,
josta suvusta siitten yksi nimeltä Åke Axelsson Natt och Dag tehtiin
v. 1652 Vapaherraksi 23:nen N:on alle. Se oli silloin Valta-Neuo ja
Lain-julistaja Nerkissä, ja sai vapa-moaksensa muutamia taloja ja
vero-tiloja Iin pitäjässä Pohjan ruoalla.
[600] Saattaa ehkä myös olla madollinen, että hyö ovat
perinpohjin eri-sukuja, vaikka heitä on vanhoissa polvi-laskuissa
yhteen veittynnä.
[601] Hään oli silloin Valta-Neuo Ruotissa.

[602] Hänen isänsä oli Bó Sténson (Natt och Dág) joka v. 1440 oli
nainut Kárin Svennintytärtä Stúre, jonka isä oli Tähti-mies ja
Linnanisäntä Faeholmassa, Danmarkissa, Sven Sténson Stúre, joka
oli Herttu Albrechtilta soanut isoja pito-maita Hallannissa, Nerkissä ja
Vester-Norrlannissa; ja joka oli Valta-Hallihtian Svante Stúrin isän-
äitin-isä (lue Schönefeltin matrikel).
[603] Seneistäpä kaikki nykyiset Vapaherrat nimeltä Stúre, ovat
kaikki isänsä puolesta paljaita Natt och Dagiloita, ja ovat eroitettavat
niistä vanhoista Stúriloista, joita muinonkin kuhuttiin: Orms-Söner.
[604] Lue C.F. Schönefelts Matrikel öfwer ointroducerade af
Riddersk. och Adeln I D. joka kirja löytyy käsikirjoituksenna K. Vapa-
Huoneessa.
[605] Lue Olai Magni Historia de Gentibus Septentrionalibus,
Romae 1555. Lib. II. c. 25. p. 87. Kussa hään puhuu niistä vanhoista
Hangöin kallioloissa sisään-hakatuista Suomalaisista vapa-
merkkilöistä, joita hään jo silloin kuhtui "vetustissima" (varsin
vanhoja) ja joista hään kuvittaa 7 kappaletta, nimittäin: Vanhoin
Stúriloihen, Natt och Dágiloihen (poikki-puolin), Wásaloihen,
Gyllenstjernilöihen, Tottiloihen, Roosiloihen, Lämaloihen ja yhen
tunnettoman. Näitä kaikkia on hään asettanut vempelen näköiseen
poukkamaan, ja keskellen pannut Ruotin vallan vapamerkin (kolmet
ruunua).
[606] Tämä hautakivi mahto jo 1681:nen tahi 1738 vuuen
tulipalossa hävitä, koskei siitä mainitak niin mitään Lauraeuksen
Juttelemuksessa de Sacellis Sepulcr. in Templ. Cath. Aboënsi. Kussa
ainoastaan sanotaan yhen Lainistujan Natt och Dágin (hänen
Ristimä-nimeänsä ei nimitetäk) olleen hauattunna Piispa Tavastin
hauta-kammiossa.

[607] Lue: Åbo Tidn. 1785. Bib. p. 181. Siinä ei eroitetak, jos hään
oli Natt och Dag pitkinpäin tahi poikkipuolin; mutta mahtoi se olla
pitkinpäin, koska yksi hänen jälkimmäisistä nimeltä Niclis
Ærengislesson kuhuttiin Natt och Dag i längden.
[608] Tällä Koarle Näskonungssonilla oli yksi veli Ærengisle
Näskonungsson (Natt och Dag) joka v. 1312 oli Miekka-mies, Ruotin
Valta-Neuo ja Vallan-Asettaja, ja yksi Roskildin Rauhan-Toimittajoista
(en ibland Freds-Kommissarierna wid Roskilska freden). Häntä tehtiin
v. 1323, Vallan-Asettajaksi Norissa, ja v. 1324 Ruhtinaaksi Ruotissa.
Hänellä oli yksi poika Ærengisle Ærengislesson, joka oli Miekka-mies,
ja jonka jälkimmäisistä arvelemme sitä Niclis Ærengislessonnia, jota
nimitettiin "Natt och Dag i längden", joka oli nainut Karin
Knútintytärtä, ja jolla oli Tukhulmissa monet talot, jotka se pois-
lahjotti niillen tässä kaupunnissa löytyivillen Papin-suljetuksillen.
Häänki mahto olla Suomen-sukuja, koska hään v. 1420 piti Valta-
käräjät Turussa (Åbo Tidn. 1789 p. 321. v. 1785 p. 233. Porth. Chr.
p. 508), ja luetteli jälkiseätöksessänsä yhtä Jeppe Finckiä,
omaiseksensa. Yksi Ærengitzle Nielsson (ehkä hänen poikansa) oli v.
1447 alakirjuttana yhtä vanhaa sovintokirjaa Göd. Finkin ja Juho
Ollinpojan veljeisten välillä (Porth. Chr. p. 448). Tämä Niiles
Ærengislesson mahto kuolla nuon v. 1440, koska hään silloin teki
jälkiseätöstänsä (sitt testamemte). Sekä hään että Ærengisle
Niclisson, oli kumpaisetkin v. 1436 ylös-pantu heijän joukkoon, joita
Kuninkaan Christofferin koroitus-päivällä v. 1441 piti tehtämän Tähti-
niekoiksi (Porth. Chr. p. 607). Myö aprikoime ellei tämä Turun
muinonen Pappi lie ollut varsin tästä sukupolvesta. Hänen ristimä-
nimensä Niiles on aivon Stúriloihen (eli niiten nuortein Natt och
Dágiloihen) kuin myös niiten vanhoin Natt och Dágiloihen, kaima-
nimi. Mutta yhtä Antin nimellistä, joka oisi ollut hänen isänsä, ei
löyetäk koko tässä sukukunnassa; niissä muka polvi-laskuissa, jotka

luetaan Vapa-Huoneen nimi-kirjoissa (Matriklar). Mutta meijän tuloo
muistuttoo, että hyö ovat ylikynteen varsin puuttuvaisia ja viallisia,
erinomattain vanhoista ajoista. Vuonna 1336 niin oli yksi nimeltä
Ærengisle Andersson Suomenmoan Peämies, eli niinkuin heitä silloin
kuhuttiin "Advocatus Finlandensis." Hään kuhtuu ihtesek yhessä
vanhassa Peätöskirjassa Stensbölin kartanosta, vuotesta 1335 —
Advocatus Aboënsis, ja puhuu siinä suurella kunnialla siitä ennen
mainitusta Koarle Näskonungssonista, jota hään kuhtuu "Nobilis
Miles, Dominus Carolus, Antecessor meus." Mitä sukuja hään lie ollut
on tietämätöin, mutta myö aprikoime ellei hään voan lie ollut näitä
yksiä vanhoja Natt och Dágiloita, jota hänen ristimä-nimensä ikään
kuin toistaa. Jos uskaltaisimme tätä peätteä, niin silloin oisi Antinki
nimee tavattu tässä suvussa, ja saattais muka olla mahollinen, että
hänellä oisi ollut yksi veli, tahi veljen-poika nimeltä Niiles Antinpoika,
joka oisi ollut Pappina Turussa — ellei tämä oisi elänyt, niin kuin
äsköin arveltiin, jo monta aikoa ennen.
[609] Kuninkaan Lain-Toimittaja (Konungens Domhafwande t.
Dom-innehafwande) kuhuttiin niitä Valta-Herroja, jotka Kuninkaan
siassa ja Kuninkaan nimessä pitivät Valta-käräjät (Räfste-ting)
Suomessa. Eli kuin näitä hävitettiin — ne jotka pitivät Moan-oikeutta
Turussa (Lands-Rätten i Åbo). Että hään v. 1405 piti Valta-käräjät
Suomesssa, luetaan Porth. Chr. p. 418, 508, ja Stjernm. Höfd. Minne
I D. 2 B. K I. p. 98 &c. Samaten sanotaan (yhessä Lainjulistajan
Claus Flemingin kirjassa, annettu v. 1412) hänen myöskin pitänneen
Valta-käräjöitä Ulfsbyin (Porin) kaupunnissa Suomessa v. 1410, jota
Porthan arveloopi kirjotus-virheksi vuosluvussa, luullen tämän
tarkoittavan v. 1405 (Chr. p. 418).
[610] Vara-lainjulistaja, Under-Lagman. Tämä Miekkamies Bó
Niclisson (se nuorempi) Åkeröiin oli v. 1434 Laintutkia Vaxalassa — v.

1459 Vara-Lainjulistaja Öster-Göthlannissa, ja v. 1461 Kuninkaan
Vouti-mies (Fogathe) Vedboin Kihlakunnassa ja Rumleborgin
Läänissä.
[611] Brenner: "I Åbo Domkyrkia på ett jerngaller för Biskop
Magni Olai graaf."
[612] Kammio, Kirkko-kammio Chor; Hauta-kammio, Grafchor.
Ennen Poavin aikana piettiin Turun kirkossa monta erinäistä
kammiota, kussa piettiin Jumalanpalvelusta, eli oikeemmittain, kussa
seisoi yksi altari, jonka luonna Pappiset vissinä päivinnä vuotessa
pitivät messujansa ja rukouksiansa, hyväksi niiten sieluillen, jotka
ovat näitä laitoksia seättäneet, ja heitä lahjoillansa ja antimillansa
asettaneet. Yhtenä aikana löytyi jo 18 tällaista kammiota Turun
kirkossa, joista suuri osa palkihtivat omia pappia ja messu-miehiä;
mutta kakkia näitä hävitettiin Kuninkaan Kustav I:sen aikana, jollon
tätä Poavin uskomusta pois-heitettiin. Siitä päivästä nimitettiin näitä
kirkko-kammioita paljaiksi hauta-kammioiksi, koska heissä
ainoastaan hauattiin heijän ja heijän lapsiin ruumiita, jotka olivat
heitä asettaneet, vaan ei eneä piettynä mitään henki-messuja. Piispa
Tavastin muista jumalallisista laitoksista oli yksi tämän Ristuksen
Ruumiin kammion asettaminen. Siinä häntä myös hauattiin, josta
tätä siitten kuhuttiin "Tavastin hauta-kammioksi." Tämä kammio oli
suljettu eli varuistettu näiltä rautahäkiltä, josta kuvat tässä nähään.
[613] Lue Porth. Chron. p. 429.
[614] Tämä sana fecit fieri (oli antanut tehä, tiettänyt) on yksi
Suomalaisuus (Fennicism) tässä Piispan Latinassa, joka toistaa
hänen ei ainoastaan olleen selvän Suomalaisen; mutta myös Latinata
kirjuittaissaan nouattanneen Suomalaista mielen-juohutusta. Sillä
Ruomalaiset oisivat epäilämätäk (ikeänkuin Ruohtalaisetkin)

kirjuttaneet fecit, posuit (reste t.e. stenen, minneswården). Ehkä se
oisi viallisesti sanottu, sillä Seppä teki (fecit) mutta Piispa tietti (fecit
fieri). Jos oisivat varsin tahtoneet tätä asioa eroittoo, niin oisit
kirjuttaneet tahi toimittaneet tätä apu-sanoilla (med hjelp-verber)
e.m. curavit, lät resa. Mutta Suomalaisessa kielessä ei tarvitak
sellaisia apu-keinoja, hänessä löytyy ikeän kuin Hebrealaisessa ja
Arabian kielessä, tätä eroitusta puheessa (ja ajatuksessa) toimitettu
eri-sanantaivuttamuksella (uttryckt genom en särskild
konjugationsform) jota Hebrean kielessä kuhutaan "Verbum Hiphil",
ja jota myö Suomeksi soattaisi kuhtua Tiettävä-Toimitussana
(Verbum Permissivum, t. Effectivum, t. Transitivum).
[615] Yksi kopio tästä kirjutoksesta luetaan myös Opettajan Joh.
Bilmarkin Juttelemuksessa "De Sacellis Sepulcralibus in Templo
Cathedrali Aboënsi_", Alexand. Lauraeuksen_ vastoomisella, Turussa
1772, p. 20. ja yksi toinen kopio löytyy niin ikeän Jonas Bångin "Den
Wälborna Tawastiska Släcktens ättare-tal", Stockh. 1756.
[616] Ei Porthankaan osanut näitä selittää; lue Chron. p. 511. m.
495.
[617] Joka nenä ehkä merkihtee sanaa "Regina" (Kuninkatar):
jotta ois: "Auttakoon Moaria Kuninkatar."
[618] Brenner: "I Åbo D. Kyrckia."
[619] Että tämän Piispan vapamerkki on ollut yksi semmoinen
taka-jaloillansa pystyssä seisova pukki, jota tässä nähään, arvataan
ei ainoastaan tästä hänen hautakivestä, mutta myös siitä
vapamerkin-piirutoksesta, joka hänen kunniaksi oli tehty Pargasten
pitäjän kirkko-laipioon. Sellainen Pukin-kuva on myöskin muinon ollut
kuvattu hänen muistiksensa siinä Piispan-penkissä, jonka hään oli

tiettänyt Savun kirkossa (lue Christ. Cavanderin Juttelemusta Petr.
Kalmin hoivauttamisen alla, "Beskrifning öfwer Sagu Socken." Åbo
1753, p. 3; ja Mart. N. Tolpon Juttelemusta Alg. Scarinin
hoivauttamisen alla, "De initiis Rei Litterariae in Svethia", Aboe 1750,
p. 83 etc. keskustele Porth. Chron. p. 571). v. Stjernman sanoo kyllä,
yhessä kohassa, puhuttaissa Piispan veljen-pojasta, Lainjulistajasta
Etälä-Suomessa Henrik Bitzestä, hänen vapamerkkinsä olleen
mustan veneen valkoisessa vainiossa ("en swart båt uti hwitt fält";
lue Åbo Tidn. 1785. Bih. p. 197). Mutta myö arvelemme ellei tässä
lie paino-virhe, ja että se olla pitäis: "en swart bock uti hwitt fält."
(Keskustele Porth. Chron. p. 545). — Uggla sanoo taas näihen
Bitziloihen vapamerkin olleen yhen Hirven, ja rautalakissa 4 sisään-
pistettyä nuolta (Uggla, Sw. R. Rådslängd n. 663. p. 65); mutta ei
häänkään nimitäk minkä perustuksen peällä hään tätä sanoopi.
Koskei tämä Bitzin suku löyvyk K. Ruohtalaisessa Vapa-Huoneessa
sisään-otettu, eikä hänen vapamerkkinsä heijän vapakirjoissa
piiritetty, niin meijän täytynnöön ottoo kirjaamme mitä ovat tästä
kirjuttaneet, että siitä tutkia totuuen.
[620] Porth. Chron. p. 26.
[621] Porth. Chron. p. 586.
[622] Hauta-kirjutos, Grafskrift, Epitaphium.
[623] Se kuuluupi näin: "Sanct. Venerabilis Patris, Domini Conradi;
Episcopi Aboënsis, anno 1489 den 13 Martii."
[624] Ruotiksi kirjutettiin hänen nimensä usseemmittain (sanan-
supistamisella) aivan lyhykkäisesti: "Biskop Koort, Korth, ja Kort."

[625] Piispa, joka oli myöskin ollut yksi osallinen Kolmen
Kuninkaan Veljellisyyestä, Turussa, ei laimin-lyönyt piteä kirkkonsa
puolta, eli valvoa hänen hyötymisestään, kussa oli voan mitään
etullista soatuvilla. Niin kuin Peä-Rovasti pisti hään jo v. 1459
nimensä hänen enonsa Arvidh Claussonin jälkeen-seätöksen ala,
kussa hään Kolmen Kuninkaan Kammiollen (altari Trium Regum)
poislahjoitti tilansa Sorkisten kylässä Euran pitäjässä (Porth. Chr. p.
456). Samana vuonna alakirjutti hään myös saman enonsa lahjutos-
kirjan, kussa hään Pyhän Ristuksen ruumiin Kammiollen (Altari
Corporis Christi) pois-anto tilansa Pärkiö Vehmaan pitäjässä (Porth.
Chr. p. 434). Vuonna 1484 alakirjutti hään niin-ikeän Vapamiehen
Járl Jönssonin seätöksen, kussa hään sovinoksi Hárald Ollinpojan
murhasta, anto tilansa Kivikylä Virmon pitäjässä Kaikkein Ristuksen
Uskollisten Henkein Kammiollen (Altari Animarum Christi Fidelium)
(Porth. Chr. p. 442.), monta muita mainihtamatak. Ite hään ei
seätänyt kirkollen paljo mitään, jos ainoastaan toimitti isän
vainoonsa tahtoa (Åbo Tidn. 1785 p 199. keskustele Porth. Chr. p.
551 & 622).
[626] Tämä vanhaksi mainittu Eerik t. Henrik Bitze, on nimensäk
suhteen paha eroittoo hänen pojasta ja pojan-pojasta, jotka
kantovat saman nimen, ja joihen kanssa häntä ehkä sevoitetaan.
Hänen sukunimensä kirjutetaan monella tavalla, sekä Biidz, Büdz,
Bitz, Bytz, Bitzr, Bitze että Bisse (Porth. Chr. p. 543, 481,) ja se
näyttää kuin sillä tarkoitettais yhtä kuin sanalla Bässe, (jota hään
kantaa vapamerkissänsä). Juusten kuhtuu tätä Piispan iseä "famosus
Miles, quondam Capitaneus Castri Aboënsis." Hään oli jo v. 1420
Miekkamies (Armiger) ja v. 1441 Tähtimies (Miles). V. 1437 oli hään
Laintutkia Halikon kihlakunnassa, jota virkoo hään piti aina vuoteen
1453, jollon häntä myös kututaan Laintutkiaksi Vehmaan
kihlakunnassa. Samana vuonna mainitaan häntä myös

Lainjulistajaksi Pohjos-Suomessa, ja vuonna 1455, 1456 ja 1457
kuhutaan häntä jo Lainjulistajaksi Etelä-Suomessa (Lagman i
Sudhersinne Laghsagu); ja v. 1449 häntä jo nimitetään Ruotsin
Valta-Neuoksi, jollon häntä s. 31 päivänä Heinä-kuussa Visbyin
kaupunnissa alakirjutti Kuninkaan Koarle VIII:nen ja Christian I:sen
sovintoa Gottlannin soaresta (Hadorph efter Rimkrönikan p. 156.)
von Stjernman sanoo hänen myös v. 1452 olleen Turun linnan ja
moakunnan Peämiessä (Åbo Tidn. 1785. Bih. p. 198. Porth. Chr. p.
544). Hään eli vielä v. 1458, vaan oli jo kuollut ennen v. 1467, ja oli
ollut osallinen siitä Turussa löytyvästä henkellisestä Kolmen
Kuninkaan veljellisyytestä (Porth. p. 476, 545). Hänen iseensä ei
tunnetak, ja hänen äitinsä (jonka nimee ei muistetak) oli Turun
ensimmäisen Peä-Rovastin (Domprost) Heikki Maunuksenpojan sisar.
Hään oli kuolemaisillaan, jälkeen-seätöksessänsä, pois-lahjoittanut
tilansa Kuirilahen kylässä Paraisten pitäjässä, sillen Turun
Peäkirkossa asetetullen Pyhä Pietarin ja Pyhä Poavalin Kammiollen
(Porth. Chr. p. 445. Åbo Tidn. 1785, Bih. p. 199). — V. 1435 oli hään
vierasmiessä alakirjuttanut appensa Clauus Lydikinpojan seätös-
kirjoo, jolla hään Papis-kammiollen (eli niin kuin sitä muinonkin
kuhuttiin, "Neitzyn-kammiollen") Turun Peä-kirkossa, poislahjoitti
Hukasten taloo Lemun pitäjässä, m.m. (Porth. Chr. p. 453); ja v.
1438, oli hään niin ikeän ala-kirjuttanut Turun Peä-Rovastin Matti
Ollinpojan lahjutos-kirjan, jolla hään Pyhä Annan Kammiollen
poisanto Littoisten tilan Nummen pitäjässä (Porth Chr. p. 448).
Samana Vuonna istui hään Laki-miessä (såsom bisittare eller nämd i
Konungens dom) Moan Oikeutessa (wid Lands-Rätten) jota piettiin
Turussa, ja kussa häntä kuhutaan Laintutkia Vehmaan kihlakunnassa
(Åbo Tidn. 1785, Bih. p. 63). Vuonna 1449 vahvisti hään niin kuin
Turun muinoisen Peämiehen Heikki Gärdshaghin vainaan lasten
holhottaja (förmyndare,) sen kauppa-kirjan, jolla hään oli eläissänsä

myönyt tilansa Keykalan kylässä Kalvolan pitäjässä Hämeenlinnan
Vouvillen Engelbrecht Jaakonpojallen, 60 markkaan (Porth Chr. p.
525).
[627] Porth. Chr. p. 481, 453, 543. Tämä Anna Claus-
Lydikintyttären (Djäkne) isä, oli se Clauus t. Niiles Lydhekeson, jota
jo p. 424 nimitimme, ja jonka v. 1407 sanotaan olleen Laintutkiana
Pohjos-Suomessa, ja v. 1414 ja 1420 Voutina (Foghot, Fogda) Turun
linnassa. V. 1420, 1429, 1430 ja 1434 kuhutaan häntä myös tämän
linnan Peä-mieheksi (Höwitsman); ja v. 1442 Capitaneus Castri
Aboënsis (Åbo Tidn. 1785, Bih. p. 191, 192). Hänen sanotaan tulella
yläs-polttaneen oman vaimonsa nimeltä Christina Jonisedotteria,
joka vielä eli v. 1435. (Porth. Chr. p. 453). Ilman tätä Annaa, joka
mahto olla nuorin hänen lapsistaan, oli 7 muita; nimittäin: — 1)
Tähtimies Henrik Clauson (Djäkne) Koskiseen, joka oli Valta-Neuo ja
Lain-julistaja Pohjos-Suomessa (Lagm. i Norrsinne Laghsagu)
voutesta 1449 vuoteen 1458, naitu Lucia Ollin-tyttären (Tavastin)
kanssa; — 2) Arffwidh Clausson Nynäsiin, Tähtimies ja Valta-Neuo,
naitu Ingeborg Arend-Pentinpojan tyttären kanssa; — 3) Tönne (t.
Antonius) Clausson; — 4) Britha Clausdotter, Herreilään (?) naitu
Heikki (Pekanpoika) Svärdhin kanssa, joka eli v. 1420, ja jollen se
synnytti yhen tyttären, nimeltä Ragnild; — 5) Karin Clausdotter
Kankkaan, ensin naitu v. 1407 Jaakko (Niileksenpoika) Kurkin
kanssa, jollen se synnytti yhen pojan Claes Kurck Laukkoon, joka eli
v. 1466; ja siiten Heikki Ollinpoika Hórnin kanssa Åminneen, joka oli
Hórniloihen Peävanhin (Stamfader, Ättefader); — 6) Elin Clausdotter,
joka oli naitu Herman Flemingin kanssa; — 7) Anna Clausdotter,
josta äsken puhuttiin; — 8) Cecilia Clausdotter, naitu Claus
Pekanpoika Flemingin kanssa Peningebyiin, joka oli Tähtimies ja
viimäinen Lainjulistaja kokonaisessa Suomen-moassa; hään eli vielä

v. 1405, ja oli niiten Suomalaisten Flemingilöihen Peä-vanhin
(Peringsköld).
[628] Claes Bitze, jolla oli yksi poika Knút Bitze Öhrestadiin, naitu
Brigitta Christjern-Pentinpojan (Oxenstjernan) tyttären kanssa
Salestadiin.
[629] Tämä nuoreksi kuhuttava Eerik Bitze Viikiin, joka myös oli
osallinen Turun Papin-veljellisyytestä (Porth. Chr. p. 476) ja jonka
Porth. p. 545, ja 638 sanoo olleen Lainjulistajana Etelä-Suomessa v.
1462 ja 1463, oli naitu Tähtimiehen Olli Tavastin tyttären kanssa,
nimeltä Märeta, jonka kanssa hänellä oli kaks lasta (Porth. luettaa p.
638 yhtä Antin nimellistä, kolmaneksi); — 1) Anna Eerikintytär Bitze,
joka oli naitu Olli Jönsinpojan kanssa., Laijsiin, ja — 2) Heikki
Erkonpoika Bitze, Nynäsiin (Porth. p. 637 kuhtuu häntä Tähtimies
nuori Henr. Bitze Nynäsiin) joka oli naitu Anna (Hannon tytär) Totin
kanssa Bjurumiin, jota usseemmittain kuhuttiin "Finska Anna på
Åkerön," ja joka synnytti hänellen kaks lasta, Eerik ja Kirsti. Tämä
Anna tuli siitten naituksi Clemet (Pentinpoika) Hogenskildtin kanssa
Åkeröiin (kuhuttu Huitfelt), ja kuoli vasta v. 1549. Tämä Henrik Bitze
joka oli Lainjulistaja Pohjos-Suomessa v. 1489, 1490, 1499, 1504 ja
1506, ja jonka Uggla kuhtuu Miekka-mieheksi Viikiin, ja sanoo olleen
Peämiessä Turussa vuotesta 1480 vuoteen 1485, ja kantaneen
vapamerkissänsä yhen hirven — oli v. 1499 Tukhulmissa
alakirjuttanut K. Christian I:sen Kuninkaan-vaalia (Hadorph p. 367).
Hään on tullut Porthanin luulon perästä (Chr. p. 545; Åbo Tidn. 1785,
Bih. p. 198.) sevoitetuksi ukkosek kanssa, joka oli hänen nimellinen.
Sillä kaikki mitä v. Stjernman puhuu Henr. Bitzestä, niin se puhuu
enin tästä nuoremmasta, ehkä hään nimittää häntä vanhaksi, ja
villitteloo sillä sekä ihtesek että muita. Se on tässä, niin kuin

moneissa muissa lopen-vanhoissa asioissa, työläästi käsittää totuutta
vielä liiaksi kuin yhtäläiset nimet meitä ereyttää.
[630] Briita Bitze Benkkalaan, tuli naituksi Olli Drákin kanssa.
[631] Knút Bitze, Häänki mahto olla osallinen siitä toanon
mainitusta Papillisesta veljellisyyestä (Porth. Chr. p. 477).
[632] Oppia, Magister; Tietous-Oppia, Filosofie-Magister t.
Filosofie-Doktor.
[633] Tämä kuuluisa Opisto, josta on jo tullut niin monta
valaistuneita miehiä moailmaan, ja kussa Tievot ja Taijot vielä
paraittain sekä harjoitetaan että suojeletaan, tuli ensin asetetuksi v.
1409.
[634] Peä-pappinen, Abboth, kuhuttiin ylimmäinen Pappi heijän
papin-suljetuksissa.
[635] Peä-Rovasti, Domprost.
[636] Näiten Vadstenan Pappisten nimet oli Magnus, Richard, ja
Magnus Håkansson.
[637] Mitä sillä sanalla pyhittää (consecrare) tässä ymmärtänneen,
en saata varsin sanoa. Sillä koska näissä Kammioloissa jo ennen
häntä piettiin Jumalan-palvelusta, niin eivät mahtaneet olla
pyhittämätäk. Uskottava on jotakuta kirkossa tapahtuneen, joka
heijän mielestä soastutti Seurakunnan, jota nyt uuestaan pyhitettiin
— niin kuin tapa tahtoo olla Poavilaisissa.
[638] Kammion-laulaja, Chor-prest, Choralis. Turun kirkossa
piettiin Poavin aikana 6 nuorta Pappia, jotka laulelivat Jumalan-

palveluksissa. Milloin heitä ensin asetettiin on tietämätöin; mutta v.
1355 heitä jo mainitaan. Ja se näyttää kuin kukiin heistä oisi ollut
ikeän kuin Apulainen t. Lukkari auttamassa muka laulamisellansa
niitä ylhäisempiä Turun Pappiloita heijän jumalan-palveluksessaan
(Porth. Chr. p. 453, 473.) näiten lukua enenettiin siitten aikoa
myöten. Piispa Maunus Ollinpoika (Tavast) lisäisi näihin 4 uutta,
joihin Piispa Conradus Bitze vielä lisäis 2, jotka piti joka päivä
lauleleman Neitty Moarian laulu-hetket (horas canónicas) ja joillen
hään anto palkaksi papin-soatavat Nummisten pitäjästä. Niinpä jo
yhtenä aikana luettiin 12 Laulu-Pappia Turun kirkossa (Porth. Chr. p.
553). Ilman sitä vara-soalista (extra inkomst) joka jumalan-
palveluksessa, hautaisissa ja muissa semmoisissa toimituksissa, oli
heillen tuleva, niin heijän vuosillinen palkka luettiin kullenkin 10
markaksi rahassa, paihti 20 markkoo, ruokaneuoiksi, 9 mittaa
(spann) rukiita eläkkeeksi, ja 14 mittaa ohria olveksi (Porth. Chr. p.
474). Yksi mitta oli eri-maakunnissa ja erillä ajoilla erilainen, mutta
nuon arvaten luettavaksi pitävä 24:nestä 32:neen kappaan.
[639] Poto-huone, Hospital, sjukhus.
[640] Tämä Köyhäin Tivunti, johon luettiin neljäs osa Kirkko-
rahoista ja Pyhä Henrikin otosta, ja joka kussakin seurakunnassa
alussa annettiin Kirkko-vaivaisillen, oli jo ennen Ruotissa niinikeän
pois-annettu näillen poavilaisillen Papis-Neuoittelioillen, (Canonici).
[641] Henkellinen Opettaja, Theologie Professor.
[642] Kirjan-painaminen, joka on se isoin ja avullisin taito, johon
meijän ymmärrys on yltynyt, tietomuksiin harjoittamiseksi ja
ihmiskunnan henkelliseksi valaistukseksi, ilmauntui 49 vuotta tätä
ennen Saksan-moassa, kussa yksi vapasukuinen mies nimeltä Johan
von Sooyenloch, eli muuten myös kuhuttu Gänsefleisch vom

Gutenberge, tahi niin kuin häntä jokapäiväisessä puheessa kuhutaan
Guttenberg, rupeisi ensin monen kokemuksen perästä,
kuurmaelemaan kirjotus-neniä irtonaisiin puupalaisiin, joita hään
asetti lomaksuttain sanoiksi. Ja koska puu oli arka kulumaan, niin
hään kirjutti näitä neniä ly'y-palaisiin, joihen peälle hään siitten
painutti paperinsa. Tällä tavoin tuli v. 1439 se ensimäinen kirjan-
paino toimeen Wittenbergin kaupunnissa. Koska hään näihin
kokemuksiin oli hukuttanut kaikki omaisuutensa, otti hään Appensa
kumppaliksensa, joka oli yksi rikas kulta-seppä Mayntzin
kaupunnista, nimeltä Johan Faust. Tämäpä otti toas kaks muita
toveriksensa, nimittäin veljensä Jaakko Faust ja yhen pappisen,
nimeltä Schöffer, joka v. 1452 rupeisi valamaan näitä neniä tinaan,
ja kohta siitten kovempaankin kasariin (metall). Viekkauellansa ja
kavaloilla juonillansa omisti Faust tämän rehellisen Guttenbergin
kirja-pajaa, ja lopetti v. 1462 sen ensimmäisen Roamatun painamista
Latinan kielellä, josta hään sai paljon rahoo, alinomattain Parisissa;
suureksi harmiksi Pappisillen, jotka Roamatun kopioittamisella oli
tähän saakka viljellut paljon rahoja.
[643] Tässä Suomalaisessa Messukirjassa on alku-lehellä (på tittel-
bladet) puu-kuurmauksilla (i träd-snidt) kuvaeltu yksi istuvainen
Piispa, jolla on kypärä peässä, ja oikeassa käessä kirja, vasemmassa
Pispan-sauva, joka jaloillansa poljee yhtä miestä, joka makoo
pitkällänsä, kerityllä peällä, pitävä myssynsä vasemmassa käessä, ja
oikeassa kirveensä. Tämä kuvaus joka tarkoittaa Ristin uskon
ensimmäistä levittämistä Suomessa, ja joka tarinamuksessamme
muistuttaa meitä Piispa Henrikin pyhittämistä kuoltuaan — näyttää
niin kuin se ois muka kopioitettu siitä Hauta-kivestä jota Piispa
Tavast asetti Peä-Piispan (Erke-Biskop) Henrikin hauallen Nousisten
kirkossa, ja josta siitten on malli (modell) otettu niihin malauksiin

jotka oli tehty Iso-kyrön kirkossa Pohjan moalla, josta tullaan
puhumaan XXIII:ssä Taulussa.
[644] Näistä so'ista puhutaan aivan vähä meijän
Tarinamuksessamme, koska heitä piettiin enemmin rajan
murtamisella kuin oikeellä soan-käymisellä. Heitä piettiin aina
vuoteen 1468, jollon tehtiin vara-rauha, mutta ei se pitänt jos 5
vuotta; sillä v. 1473 puhkeisi toas sota, ja muuttui aina julmemmaksi
kumpaisellakin puolella, eikä helpount Eerik Akselinpojan sisään-
murtaamisella Venäjäseen v. 1480, eikä Stén Stúrin soan-käynöllä v.
1488.
[645] Tämä Eerik Axelsson Tott (josta vasta tullaan enemmin
puhumaan) oli sama mies joka näinä aikoina ensin varusteli Viipurin
kaupunkia kivi-muuriloilla (lue XX Taulu).
[646] Nämät puu-varustukset tehtiin v. 1475, paraassa sota-
aikana, ja juuri vihollisten kuuluvissa, niin kuin Tott tästä ite
kirjuttaa: "och när arbetis folket moste fara efter sand, steen och
kalck, då måste jag hafwa en roote med hwar pråm, och 12 eller 14
mine egne tjänare med harnesk oc hwärjor för Ryssarnes skuld."
(Porth. Chr. p. 594).
[647] Lue Porth. Chr. p. 581. Åbo Tidn. 1793, N:o 15. Juvan pitäjä,
joka jo v. 1442 sai oman Papinsa, luettiin silloin kappelina Savilahen
tahi Mikkilin pitäjäseen (lue Åbo Tidn. 1784, p. 385. Porth. Chr. p.
515.) mitenkähän se oisi siitten eneän tullut kuuluvaksi Seäminkiin?
[648] Se on kumma ettei Juusten puhuissaan tämän Piispan
ajoista, niin sanalla nimitäk näistä Turun kirkon tuli-paloista. Tahi hyö
eivät olleet varsin turmiolliset (förhärjande) tahi luettaa hään heitä
siihen, jonka hään sanoo tapahtuneen iski-tulella v. 1458 Piispa

Olaijin aikana, ja josta toas ei Messenius, eikä tämä vanha ajan-
laskettaja, tiijä niin mitään.
[649] Niin e.m. tuli Iin pitäjä vasta vuuen 1475:nen tienoilla
eroitetuksi Kemistä; ja Akkas v. 1483 eroitetuksi Seäksmäestä.
[650] Brenner: "I Åbo D. Kyrckia."
[651] Tämä vuosiluku on vissiinik viärin kirjutettu, ja pitäis olla
1454, niin kuin kohta kuullaan.
[652] Kärsiäjä, martyr, Pyhät kärsiäjät, de heliga martyrer.
[653] Yrjön t. Yrjän-päivä, oli s. 24 p. Huhti-kuussa.
[654] Mikä mies hään lie ollut, ei heissä selitetäk, eikä myös hänen
isänsä nimeä.
[655] Tämä Hórnin suku-juoksu (stamtafla), joka myös löytyy
niissä vanhoissa Péringsköldin, Åkersteinin, v. Schantzin ja
Palmsköldin polvi-laskuissa (Genealogier), selittää että Vapa-mies
Clas Heikinpoika Hórn Åminneen, joka v. 1485 oli Laintutkia Halikon
kihlakunnassa, ja v. 1487, 1488, 1490, 1499, 1508, 1510 ja 1514
Lainjulistaja Etelä-Suomessa, ja v. 1499 Ruotsin Valta-Neuo — oli
naitu Christina Frillen kanssa Hoapaniemeen, joka oli Lainjulistajan
Etelä-Suomessa Christian Håkansson Frillen tytär. Palmsköld, joka
myös kertoo tätä, sanoo että tämä Hórn oli vielä toisen kerran naitu
Christina Antintytär Karplanin kanssa. Merkillinen on että vaikka
hänellä oli kaksi vaimoa Kirstin nimellä, niin eivät kuitenkaan ykskään
heistä ollut Frésen sukuisia, ellei heijän nimet lie viärin toimitetut.
Mahollinen oisi ehkä myös, tällä Hórnilla olleen vielä kolmaaskin
vaimo, samalla kaima-nimellä. Jos otamme ajan-luvusta vuoaria, niin

havaimme kohta että tässä mahtaa jossa kussa olla erehtys. Sillä jos
tämä Frese oisi elänyt 1300 vuosien alulla (niin kuin luetaan hänen
hautakivessä) niin mitenkä hänen pojan-tytär oisi ollut naitu tämän
Hórnin kanssa, joka vielä eli 1500 vuosien alulla, eli oisikkohan
kolmet suku-polvea ylettänyt kahteen sataan aastaikaan? Sillä tahi
tässä on tehty Frési 100 vuotta vanhemmaksi (kuin hään olla pitäis),
tahi se on sevoitettunna siiheen nuorempaan Frésiin (joka on muka
yhtä) tahi ymmärretään tässä yhtä toista Hórnia kuin tätä äsköin
mainittua; ehkei yhtä toista sillä nimellä ouk ollut Lainjulistajana
Etelä-Suomessa. Myökin oisimme uskomoisillamme että yksi Frése oli
naitu yhen Hornin kanssa. Mutta jos tämä oli Claes nimeltään, eli jos
hään oli Lain-julistaja Etelä-Suomessa, sitä emme saata sanoa
(Pahuus kuin ei niissä Vapa-Huoneen kirjoissa nimitetäk minkän
perustuksen peällä hyö ovat näitä puheita kirjaan pistäneet). Meijän
luulo luottaiksen sen peälle, että Maskun pitäjän kirkon ikkunassa oli
muinon moalattu Hórnin ja Frésin vapamerkit rinnattain, josta
arvattaisiin, että hyö ovat olleet naimisen kautta yhistetyt, ja että
hyö ovat tässä pitäjässä asunneet, tahi että heillä tässä on ollut tiloja
ja kartanoita (kaho XX:nees Taulu N:o 2 ja 3).
[656] Koska myös tämä kaikki ikeän kuin passoisi tähän Fredr.
Fréseen, jonka hautakivi tässä kahellaan, vaan joka nyt luetaan 100
vuotta vanhemmaksi, niin milt' emme epäile Brennerin tässä
lukenueen veärin, ja vuosluvun ehkä olleen MCCCCLIIII, liioiten
koska tämä kivikin näyttää olevan teoiltaan niiten toisten kanssa
yksi-ikuinen, vaan ei sunkaan vanhempi; ja koskei Brennerin aikana
löytynyt Turun kirkossa muitakaan hauta-kiviä 1300 vuos-luvulta,
jotka kaikki ehkä lie murentuneet Turun kirkon tuli-palossa v. 1458
(Juusten; mutta v. 1464, 1473? Messenius) niin on uskottava ettei
tämäkään ouk niin vanha kuin hänessä luetaan. Se näyttää kuin
Brenner oisi jo itekkin tätä arvannut, sillä siinä nioitetussa kirjassa on

hään kirjuttanut vuos-luvuun: "MCCCCLIIII" niinikään luetaan myös
tätä vuoslukua yhessä vanhassa puu-kuurmauksessa tästä hauta-
kivestä. Mitä taas Vapa-Huoneen kirjoitukseen tuloo, kussa luetaan v.
1354 niin se ehkä luottaiksen tämän Brennerin vanhimmaisen
piirutoksen peälle, jonka olemme kopioittanut.
[657] Kolmen Kuninkaan Veljellisyys (Fraternitas Trium Regum)
kuhuttiin sitä papillista yhteyttä tahi veljellisyyttä, josta jo puhuttiin
p. 375, 377.
[658] Peä-Neuvo, Borgmästare. Hään oli ollut Peä-neuona v. 1431,
1439, 1448 ja 1449; ja luettiin olleen Saksalaisesta suku-perästä
(Chr. p. 598).
[659] Brenner: "I Åbo D. Kyrckia."
[660] Tämä Vapamerkki muutettiin siitten yheksi mustaksi Yötyr-
peäksi valkoisessa vainiossa. Mutta milloin, eli keltä, tätä tehttiin, on
tietämätöin. Bång sanoo kyllä (Palmsköldin puheen peälle; kaho p.
441): "Olof Niclisson Tawast upptog sin Frus, de gamble Finckars
sköldemärken, ett swart Syltehufwud i hwitt fält, sådant som Asessor
Brenner afritat det i Åbo D. Kyrka, litet förrän kyrkan bran." Mutta
näissä puheissa on niin paljon valetta, ettemme ollenkaan heihin
uskotak. Sillä — ensinnik niin tämä Olli Niileksenpoika Tavast ei ollut
naitu Finckilöihen kanssa — toiseksi, niin Finckilöihen vapamerkissä
ei ollut mitään Sian peätä — kolmanneeksi, niin nähään vielä tästä
Olli Niileksenpojan hauta-kivestä, jotta ei hään vielä
kuolemaisillaankaan ollut pois-muuttanut sitä vanhoo suku-
merkkinsä, ja — neljänneeksi niin näissä Brennerin piirutoksissa ei
löyetäk yhtä sellaista kuvattua Kössin-peätä, josta tässä puhutaan.
Tämä vanha merkki ei vielä ollut sen eistä tämän Ollin aikana pois-
heitettynnä; mutta 100:a'an vuuen peistä oli jo muutos tapahtunut.

Sillä Arvid Heikinpoika Tavast Wessundaan, joka v. 1568 oli
Linnanisäntänä Viipurissa, ja josta ja p. 444 puhuttiin, (ja joka oli
tämän Ollin pojanpojan-poika) kanto vapamerkissänsä yhtä Posson
peätä. Hänen aikanansa korjattiin taas tätä Tavastiloihen
vapamerkkiä. Sillä v. 1588, s. 24 p. Kesäk. niin Herttu Koarle,
kunniaksi tämän miehen pitkällisestä ja uskollisesta palvelluksesta,
paransi hänen vapamerkkinsä, sillä tavoin että, ympäri tätä Karjun
peätä pantiin yks sininen vanne kuhun oli vuorottellen pujotettu 4
punaista syväntä ja 4 punaisia luotia (kulor) — kostoksi samasta
uskollisuuestaan tuli hään monian vuuen peästä Viipurissa poikki-
hakatuksi. Tällainen tuli myöskin v. 1625 tämä vapamerkki sisään-
kirjutetuksi niihen Ruohtalaisiin Vapa-kirjoin (N:o 64) hänen
pojaltansa Germund Arvinpoiku Tavastilta Kurjalaan. Ruotissa on
nykyisinnä Peä-Luutnanti m.m. Gréve Joh. Henr. Tavast, sekä hänen
Vapaherrallisessa (N:o 321) että Grévillisessä (N:o 129)
Vapamerkissänsä, uuestaan ylös-ottanut sitä vanhoo kolmatta satoo
aastaikoa jo poishyljättyä suku-merkkiä.
[661] Sillä tämän Olli Tavastin isän-ukko, eli Piispa Maunus
Tavastin ukko vainaa, oli Herra Niiles nimeltään; josta Palmsköld
kirjuttaa: "Nicolaus Tavast Magnus, Finlandiae vir potens, habitans in
Tavastia, circa annum 1340" (Geneal. Saml. p. 3937). Mutta silloin
hään jo mahto olla keli vanha, sillä hänen pojan-poika Piispa Maunus
Olai oli syntynyt v. 1357. Hänellä oli kolm poikoo, — Olli
Niileksenpoika (Tavast, se vanhempi, sillä nimellä; ja tämän
nuoremman Olli Niileksenpojan ukko) joka oli Tavastiloihen Peä-
vanhin, ja jota Juusten kuhtuu: Nobilis et famosus Vasallus in
Paroecia Wirmo (Porth. Chr. p. 17, 423) joka oli Valta-Neuo ja Tähti-
niekka v. 1370, ja kuollut jo v. 1402 (Porth. Chr. p. 433) ja josta on
jo ennen p. 398 ja 422 puhuttu; — toinen oli Fader Niileksenpoika,
joka oli Stålarmiloihen Peä-vanhin, ja joka oli naitu Brita

Rochelsdotterin kanssa, ja eli v. 1370 ja 1400; — kolmaas oli Sune
Niileksenpoika, joll' oli poika Sune Sunesson, Miekkamies ja
Laintutkia Taivaansalossa v. 1402, Vehmaassa v. 1418; Valta-Neuo v.
1435, ja Lainjulistaja Pohjos-Suomessa ja Ahvenan-moalla v. 1437
(ja 1455?). Tästä selitetään mitenkä Tavastit ja Stålarmit ovat ennen
kantaneet yhtä Vapamerkkiä, vaikka eri nimellä. Kumpaisetkin suvut
oli muinon kuuluisat ja voimakkaat Suomessa, niin että löytyi harva
kirkko, kussa ei ennen aikana tavattu heijän vapamerkkiänsä
nimittäin yksi varusteltu käsivarsi, milloin keännetty oikeallen
puolellen, milloin (usseemmittain) vasemallen, osottava milloin
kämmenensä, milloin toas puistelevan nyrkkiänsä.
[662] Yksi kopio tästä hauta-kirjutoksesta tavataan Porth. Chr. p.
636. Yksi toinen kopio, jota luetaan Alex. Lauraeuksen
Juttelemuksessa Joh. Bilmarkin hoivauttamisen alla, (kuhuttu: de
Sacellis sepulcralibus in Templ. Cath. Aboënsi p. 21), on varsin
viallinen, ja kuuluupi näin: "Anno Domini MCCCCLXI crastino F:i Petri
de Cathedra Nobil. Vir Olavus Tawast, Miles hoc obiit: Orate pro eo."
von Stjernman ja Uggla eksyyvät vielä enämmin, kuin sanoovat
hänen kuolleen jo v. 1445.
[663] Istuimellansa istuvan Pyhä Pietarin päivän eli niinkuin
Ruotiksi kuhutaan tätä päivää: "Sancte Pehr i stolen," ja Latinaksi:
Petrus in Cathedra, oli yksi päivä jota poavilaiset rajuuttivat kunniaksi
Pyhä Pietarin istumisesta Poavin-tuolilla — niin kuin puhutaan heijän
satuissa. Tämä tulisi meijän luvun perästä s. 24 päivänä Helmi-
kuussa.
[664] Tämä Niiles Ollinpoika Tavast (joka oli Piispa Tavastin veli)
tuli s. 7 p. Jouluk. v. 1407 koroitetuksi Vapa-sukulliseen seätyyn,
Kuninkaalta Eerikiltä Pommerista, hänen Turussa ollessaan. Hään eli

vielä v. 1415 ja 1423. Hänen perillisistä mainitaan yhtä Vapamiestä
nimeltä Heikki Tavast, joka v. 1457 sai Valta-Hallihtialta Eerikki
Axelinpojalta vapaallista vapautta (frälse-frihet) niihen verotiloin
peälle, joita hään oli ostanut talonpoijilta Halisten kylässä
Räntamäen pitäjässä, ja Hekkialan kylässä Nummen pitäjässä (Porth.
Chr. p. 420, 421).
[665] Tästä Suomen Piispasta, josta on jo vähä mainittu p. 396,
461, 468, 482 tullaan koht-sillään enemmia puhumaan VI:nessa
Taulussa.
[666] Keskustele Porth, Chr. p, 636. v. Stjernman, joka myös
luettaa häntä Hämeenlinnan Linnanisännistä, sanoo hänen jo olleen
siinä Linnanisäntänä v. 1444, jä tässä virassa kuolleen v. 1445 (lue
Görwells' Sw. Mecurius v. 1757, Sept. p. 270; Porth. Chr. p. 521, 636;
Ugglas Rådslängd III Afd. s. 55). Mutta tässä ensimmäisessä
puheessa ei mahak ehkä olla parempata perustusta kuin siinä
viimeisessäkään.
[667] Lue Åbo Tidn. 1785, Bih. p. 192; Porth. Chr. p. 521: Koko
tästä rauhasta ei tunnetak meijän Tarinamuksessa niin mitään, ei ies
minä vuonna sitä tehtiin. Myö soamme vastapäin tilaisuutta että
kirjassamme Handl. till uplysning i Finlands äldre Historie toimittoo,
jota siinä viis-vuotisessa vara-rauhassa, jota tehtiin Viipurissa v.
1468, nimitetään että se entinen rauha oisi muuten loppunut v.
1469, s. 1 p. Toukok. Jos nyt varoisimme tämän rauhan olleen tätä
äsköin nimitettyä 9:sän vuotista, niin se oisi tehtynnä Toukokuussa v.
1459, ja oisi tapahtunut vuotta ennen tämän Tavastin kuolema-
vuotta. Hänen lankonsa Heikki Niileksenpoika Diekn, kuoli jo syksyllä
v. 1459.

[668] Tämä Porkalan Herras-kartano (Janakkalan pitäjässä?), oli
vanhuuestaan ollut Tavastiloihen moisio, mutta tuli tämän Ollin
sisaren kautta, (nimeltä Katrina Niileksentytär Tavast Porkkalaan)
annetuksi hänen avio-miehellensä, sillen vanhallen Gödik Finkillen
(lue p. 421) jolta se nyt (v. 1439) lie tullut takaisin-lunastetuksi,
koska se siitten tämän Ollin tyttären kanssa, (nimeltä Märta
Ollintytär Tavast Porkkalaan), annettiin hänen toverillensa, Valta-
Neuollen ja Lainjulistajallen Etelä-Suomessa, Jaakko Pekanpojalle
(Ille) Storgårdiin. Sillä tavalla tuli tämä hovi jo kuuluvaksi Illilöillen.
Hänen poikansa, Linnanisäntä Stén Jepinpoika Ille Porkkalaan, anto
tämän talon v. 1509 huomen-lahjaksi vaimollensa Anna
Knútintyttärellen (Kurck) Laukkoon (lue p. 431). Hänellä oli yksi tytär,
Mätta Sténsdotter Ille Porkkalaan, jota naitiin Peä-Linnanisännellen
ja Suomenmoan Holhottajallen Kustav Gödikinpoika Finkillen (lue p.
430, 431); jonka kautta tämä kartano tuli jo toisen kerran kuuluvaksi
Finckilöillen (niillen muka nuoremmillen). Kustan pojan-tyttären
kautta, nimeltä Margaréta Gödikintytär Fincke Porkkalaan ja
Auttiseen, joka naitiin Sota-Asettajallen Evert Koarlenpoika Hórnillen
Kankkaan (lue p. 405, 411) tuli tämä Herras-kartano viimen
kuulumaan Hórniloillen.
[669] Lue Porth. Chr. p. 431. Piispa lahjoitteli samana pänä kaikkia
omaisiansa kartanoilla eli rahoilla, sillä eholla etteivät milloinkaan oisi
katehtivoinnaan sitä asennosta, jolla Piispa v. 1421 perusti Pyhä
Ristuksen Ruumiin Kammiota Turun Seurakunnassa, monen talonsa
pois-lahjoittamisellansa.
[670] Peringsköld sanoo hänen olleen kahestin naitu, nimittäin
toisen kerran, Ingeborg Valdemarsdotterin kanssa (kaho p, 441)
mutta siinä hään mahtaa erehtyä.

[671] Tämä Rötgert t. Rotgert Ingosen t. Ingonpojan isä oli Valta-
Neuo ja Miekkamies Ingo Ollinpoika (Peringsk.) jonka omaisia lie
ollut Vapamies Jonis t. Jöns Ingonen joka v. 1418 ja v. 1432 istui
lakia (tingtade) Laintutkian Niiles Dieknin siassa, ja joka oli jo ennen
v. 1449 myönyt Montiskalan kartanoa ynnä muita tilojansa Raision
pitäjässä Pyhän Annan suljetuksellen samassa pitäjässä, 800:taan
Markkaan; ja josta heitä siitten syöstätiin Naantalin papin-
suljetuksen ala (Portk. Chr. p. 449, 486.)
[672] Tämä Jaakko t. Jeppe Pekanpoika (Ille) Storgårdiin oli
Lainjulistaja Etelässä-Suomessa v. 1477 ja 1485. Hänen isänsä oli
Miekkamies Pekka Axelinpoika, jonka toveri oli Ingeborg
Valdemarsdotter, joka niin muotoin oli tämän Olli Tavastin tyttären-
anoppi, ja jota Peringsköld mahtaa eräyksissä kuhtua hänen
puolisoksi.
[673] Tämä Henrik Clauusson (t. Heikki Niileksenpoika Djekne) oli
muinon yksi niistä kuuluisammista Lakimiehistä (Lagkloke)
Suomessa. Häntä ei piek sekoittoo hänen kaimansa kanssa, nimeltä
Heikki Djekne, joka v. 1374 oli Vara-Lainjulistajana Medelpadissa
(Stjernm. Höfd. Minne 1 D. p. 78, 126, 128, 139, 162, 170, 211,
224, 357 & c. Porth. Chr. p. 479); eikä häntä myös piek kuhtua
Fågelnäbiksi niin kuin Stjernman häntä nimittää lehen-laijassa (i
marginalen. Lue Åb. Tidn. 1785. Bih. p. 193) villitetty ehkä siitä
syystä, että Dieknilöihen vapamerkki löytyy Peringsköldin
käsikirjoituksissa kuvaeltunna melkeen yhelläiseksi kuin
Fågelnäbbilöihen t. Fågelhufvudloihen (jota nähään kuvaeltuna
XI:ssä Taulussa, N:o 2). Tämä Heikki, jonka isä oli se Niiles
Lydikinpoika Djekne (josta jo luettiin p. 424, 475, 476) oli jo v. 1437
Peämies Turun linnassa (Åb. Tid. 1785. p. 192) — v. 1441 oli hään jo
Tähtiniekka (Porth. Chr. p. 482. b) — v. 1445, 1446 ja 1447 oli hään

Laintutkiana Ala-Satakunnassa, ja vuoesta 1449 vuoteen 1458
Lainjulistajana Pohjos-Suomessa, joista vuosista vielä löytyy monta
hänen peätöstä (Porth. Chr. p. 527. 482. b) — v. 1449 julisti hään
lakinsa (höll han Lagmans-Ting) Birgelan kylässä Raision pitäjässä
(Porth. Chr. p. 485) ja v. 1450 oli hään muijen Valta-Neuoloihen
kanssa Arbogan kaupunnissa, kussa hään vakuutti Kuninkasta,
Koarlea Knútinpoikoo heittämään Norin hallitusta Kuninkaalle
Christjernille. Hään oli myös osallinen siitä Turussa löytyvästä
Kolmen-kuninkaallisesta Veljellisyytestä (Porth. Chr. p. 476); ja oli
näinä aikoina käynyt Appensa Tähtiniekan Olli Tavastin kanssa
Venäjässä, perustamassa yhtä 9:sän vuotista rauhoo (Åb. Tid. 1785.
Bih. p. 192). Hään oli varsin avara pois-lahjoittamaan kirkkoloillen ja
Papis- suljetuksillen tavaransa ja talojansa. Sekä tästä hänen
antamisuutesta että muutenkin myös hänen lupauksestaan,
salpataksensa vaimoneensa papis-suljetukseen, Piispa Maunuksen
kuoltua, (Porth. Chr. p. 482. b) luultaisimme hänen olleen varsin
jumalallisen. Hänen muista toimistaan tunnetaan, että hään v. 1435
alakirjutti hänen isänsä jälkeen-seätöstä, kussa hään Papis-
kammiollen Turussa anto ynnä Hukasten tilan Lemun pitäjästä, yhen
kauppa-puoin ja yhen kartanon Turun kaupunnissa, paitti 100
Englannilaista Nobloo, jonkun tilan ostoon. Siitten vaihto hään v.
1437 tämän Kammion suostumisella Olli Antinpoika Tolkin kanssa, ja
anto hänellen, ilman tätä mainittua kaupunnin kartanota, 400
Markkoo Ruotin rahassa, ja 10 kuorman alaista niittua, jonka vastaan
hään sai tällen Kammiollen Grotelan kylee Kuumon pitäjästä (Porth.
Chr. p. 453, 454). Vuonna 1448 anto hään Ajosinpeän kartanon
Maskun pitäjästä sillen äsken asetetullen Kolmen Kuninkaan
Kammiollen, jollen se myöskin v. 1449 hänen Vaimonsa
suostumisella lahjoitti yhen kartanon Turun kaupunnissa, ynnä
Atolan (Attulaby) tilan Nousiaisten pitäjästä ja Sorsalan tilan

Mynämäen pitäjästä (Dissert. de dotat. Alt. p. 9). Samana vuonna
vahvisti hään niin kuin yksi Heikki Gärdzhaghin vainajan lasten-
holhottajoista, sitä p. 475 jo mainittua kauppa-kirjoo; ja kuoli v. 1459
(Porth. Chr p. 800, 482, 483) ehkä Uggla sanoo hänen vasta
kuolleen v. 1462. Vuonna 1453 kirjutti hään Koskissa, jälkeen-
seätöksensä, kussa hään vahvisti näitä hänen entisiä asennoksia, ja
annettua vaimollensa puolen osan Koskista ynnä kaikkia hänen osto-
maita niillen säytyvillen, pois-lahjoitti hään hänen suostumisellaan
(koska hänellä ei ollut mitään lapsia) tavaroisuutensa (sin
förmögenhet) niin kuin tässä seuraa: — Peä-Kammiollen (Hög-
Altaret) Turun Peä-Kirkossa, yhen salonin (?) — Kolmen-Kuninkaan
Kammiollen Turun kirkossa, paihti kartanonsa pohjos-puolella
kaupunnissa, Atolan talon Nousiaisten pitäjästä, ja Sorsalan talon
Mynämäen pitäjästä (joita hän jo anto v. 1449) anto hään Synkalan
talon Vihin pitäjästä, ynnä yhen kalkin, joista 2 ikuista henken-
messua piti hänestä piettämän. — Pyhän-Henkein Kammiollen, yhen
kolm-jalkaisen pa'an. — Pyh. Henken Huoneellen (Helge Ands huset)
2 Lehmeä, 2 Lammasta, 2 L. Rukiita, ja 2 Liikkiöä. — Poto-
Huoneellen (Spitalet) sitä samoo. — Pyh. Laurentiuksen Kirkollen
Vehmaassa, yhen Hevoisen. — Pyh. Uolovin Kirkollen Ylälässä, yhen
Kammio-kauhtanan (Chor-kappa) ja yhen 16:nen kuorman alaisen
niityn Latvassa, jota hään oli ostanut Heikki Heikalalta 12:lla
Markalla. — Naantalin Papis-suljetuksellen (jollen se oli jo ennen
antanut puolen Aijlosen talosta) yhön kullatun vyön, ja yhön soaren
nimeltä Lethis. — Pyh. Uolovin Suljetuksellen Turussa, yhen niitty-
moan Letzalassa, ja hänen isoimman kupari-kannunsa. — Raumon
Suljetuksellen, puolen sälytyksen (Läst) Rukiita, 2 Lehmeä, ja 2
Liikkiöä. — Musta-Veljeisten Suljetuksellen (Swart-brödra Klostret)
Viipurissa, yhen hopea-maljan. — Harmaa-Veljeisten Suljetuksellen
(Grå-brödra Klostret) samassa kohin, yhen kulta-sormuksen. — Pyh.

Brigittan Suljetuksellen Kesoin kaupunnissa (t. Reävälissä) 20
Markkoo, jotka hänen piti soaha Claus Pekanpojalta Reävälissä,
kahesta hevoisesta. — Musta Veljeiksillen Kesoissa, yhen harmaan
hevoisen. — Pyh. Henrikillen, hänen parhan Ruunansa ja Rauta-
paijansa. — Pyh. Henrikin hauallen Nousiaisessa, yhen hurstin t.
peitteen. — Koarle Kuninkaallen, yhen valkean ja ruuninkarva-
kirjavan Hevoisen. — Piispa Uolovillen, yhön pöytä-liinan, ja hopea-
vaipan. — Hänen siskonpojalle Peä-Rovastillen Opp. Kort Bilzille,
yhen hopea-lukotun kannun (kansa?) — Peä-Kirkonpalveliallen
Turussa, yhen hopea-maljan. — Opp. Arvid Jaakonpojallen, yhen
maksankarvaisen käymärin (gångare). — Opp. Maunus
Valdemarinpojallen, yhen hopea-tuopin, ja yhet parit Herkiä. —
Veljellensä Arvid Niileksenpojallen, hänen hopea-vyönsä
(kullattumatoin), ja yhen mustan varsan. — Herra Niiles Naebbille,
yhen pienen hopea-vakan (silf-kosa). — Herra Niiles Mullillen, yhen
hopea tuopin. — Herra Niileksellen Pietarsoaressa, hänen mustan
kauhtanansa, Niätän-nahoilla kalsattuna (befodrad). — Herra
Knútillen Vehmaassa, yhen Härän, ja yhen mustan kauhtanan. —
Rötkerillen Vehmaassa, yhen rihla-pyssyn, yhen pa'an, yhen kattilan,
yhen kannun ja 4 lammasta — Herra Heikki Vilmarillen, yhen sänky-
voatteen, yhen parin Härkiä, ja yhen kannun. — Olli Dúsillen yhen …
sänkyn, yhen kannun, yhen pa'an, yhen kattilan, 2 Lehmeä, ja yhen
Härkä-parin. — (Heikki?) Plátallen, 2 Härkeä. 4 Lammasta. — Pekka
Karpalaisellen, hänen hopia-peä lukkoisen veihtensä. — Ovikonpojan
perillisillen Vihin pitäjässä, yhen niityn, jonka hään osti Plátalta 6:lla
Markalla. (Åb. Tid. 1785, Bih. p. 193. Åbo Stifts Predikare-Bröders
och Nådend. Klost. bref T. VI. p. 1362. Yksi käsikirjutos, joka löytyy
K. Vallan Säilyksessä, Tukhulmissa).
[674] Lue Porth. Chr. p. 424. m. 379; p. 456. m. 702. p. 484. m.
448. p. 529. — Gr. Hallenii Dissert. praes. Alg. Scarin de Virmoëns. in

Welcome to our website – the perfect destination for book lovers and
knowledge seekers. We believe that every book holds a new world,
offering opportunities for learning, discovery, and personal growth.
That’s why we are dedicated to bringing you a diverse collection of
books, ranging from classic literature and specialized publications to
self-development guides and children's books.
More than just a book-buying platform, we strive to be a bridge
connecting you with timeless cultural and intellectual values. With an
elegant, user-friendly interface and a smart search system, you can
quickly find the books that best suit your interests. Additionally,
our special promotions and home delivery services help you save time
and fully enjoy the joy of reading.
Join us on a journey of knowledge exploration, passion nurturing, and
personal growth every day!
ebookbell.com

Fme 2001 Formal Methods For Increasing Software Productivity 2001th Edition Jose N Oliveira

About This Presentation

Slide Content

Tags

Categories

Download

Quick Actions

Statistics

Related Slideshows

Fme 2001 Formal Methods For Increasing Software Productivity 2001th Edition Jose N Oliveira

About This Presentation

Slide Content

Slide 1

Slide 2

Slide 3

Slide 4

Slide 5

Slide 6

Slide 7

Slide 8

Slide 9

Slide 10

Slide 11

Slide 12

Slide 13

Slide 14

Slide 15

Slide 16

Slide 17

Slide 18

Slide 19

Slide 20

Slide 21

Slide 22

Slide 23

Slide 24

Slide 25

Slide 26

Slide 27

Slide 28

Slide 29

Slide 30

Slide 31

Slide 32

Slide 33

Slide 34

Slide 35

Slide 36

Slide 37

Slide 38

Slide 39

Slide 40

Slide 41

Slide 42

Slide 43

Slide 44

Slide 45

Slide 46

Slide 47

Slide 48

Slide 49

Slide 50

Slide 51

Slide 52

Slide 53

Slide 54

Slide 55

Slide 56

Slide 57

Slide 58

Slide 59

Slide 60

Slide 61

Slide 62

Slide 63

Slide 64

Slide 65

Slide 66

Slide 67

Slide 68

Slide 69

Slide 70

Slide 71

Slide 72

Slide 73

Slide 74

Slide 75

Slide 76

Slide 77