Download CDET The Consistent Document Engineering Toolkit User Manual

CDET
The Consistent Document Engineering Toolkit
User Manual
www.unibw.de/inf2/CDET
Jan Scheffczyk
[email protected]
September 6, 2005
Contents
1 Introduction
1.1 What Can You Use CDET for? . . .
1.2 What is CDET not Meant for? . . .
1.3 System Requirements & Installation
1.4 This Manual . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2 Working with CDET
2
3
3
4
4
5
3 CDET System Architecture
12
4 What You need to Input into CDET?
4.1 CDET Project Description . . . . . . . . . . . . . . . . . . . . . . .
4.2 Consistency Rules . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
14
14
17
23
5 Technical Details
5.1 Project Description XML Syntax
5.2 Language XML Syntax . . . . . .
5.3 Rule XML Syntax . . . . . . . .
5.4 Repository Interface . . . . . . .
32
32
33
37
41
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
6 Future Work
A The
A.1
A.2
A.3
42
CDET Prelude
Prelude Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Prelude Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . .
Prelude Functions . . . . . . . . . . . . . . . . . . . . . . . . . . .
B DTDs
B.1 Project Description DTD consistencycheck.dtd
B.2 Rules DTD rules.dtd . . . . . . . . . . . . . . . .
B.3 Language DTD language.dtd . . . . . . . . . . .
B.4 Report DTD report.dtd . . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
43
43
43
44
47
47
49
53
59
C GNU General Public License
68
Bibliography
73
2
Abstract
When a group of authors collaboratively edits interrelated documents, semantic
inconsistencies occur almost immediately. Current document management systems (short DMS) provide useful mechanisms such as document locking and version control, but often lack consistency management facilities. At best, semantic
consistency is “defined” via informal guidelines, which do not support automatic
consistency checks.
The Consistent Document Engineering Toolkit (short CDET) aims at overcoming these shortcomings. It is a result of my research at the Universit¨at der
Bundeswehr M¨
unchen since 2002. CDET complements DMS or revision control
systems (short RCS) by consistency management. The overall goal of the CDET
is to provide a means by which you can formalize semantic consistency requirements (such as business rules), check your documents for consistency automatically, and derive repairs for inconsistencies. The crucial point is, however, to
tolerate inconsistencies, which are commonly considered a “natural” consequence
of multi-author environments.
Chapter 1
Introduction
Larger bodies of writing, such as books, technical documentations, or software
specifications, contain many interrelated heterogeneous documents. Typically, a
whole team of authors is responsible for producing and maintaining these documents. In supporting a multi-author environment, document management systems (DMS) and revision control systems (RCS1 ) store documents in repositories.
On the one hand, DMS/RCS provide fundamental management facilities, e.g.,
version management, access control, or deployment management. On the other
hand, DMS/RCS fail to manage semantic domain-specific consistency requirements. Usually, authors aim to produce an overall consistent work, i.e., certain
relations between the documents are maintained. These relations are, however,
mostly implicit and vague, e.g., “Links within documents should have a valid target.” What does “valid” mean? Why do we say “should”? Does it mean that the
rule does not need to hold always? In order to achieve consistency, authors have
to spend plenty of time re-reading and revising their own and related documents.
Worse, each check-in to the DMS/RCS potentially violates consistency. Larger
companies define guidelines and policies for writing; but still a human reviewer
is needed to maintain them. What prevents automatic consistency checks is that
guidelines are implicit or at best informal.
CDET implements a formal quality control approach that is built on top of
informal document engineering processes.2 We call this kind of quality control
“semi-formal consistency management.” CDET introduces explicit formal consistency rules to capture informal quality requirements. It does not require any
adaptations to editing practices of authors. CDET smoothly integrates consistency
management into (almost) arbitrary DMS/RCS without requiring adaptations to
document engineering processes. This is in sharp contrast to entirely formal consistency management approaches, which provide strong means for consistency management but severely hinder your work by requiring a specific document model or
format.
By “consistency checking” I mean to determine how the repository conforms
to the rules. This is in contrast to classic logic, where “consistency checking”
1
By RCS I mean an arbitrary revision control system and not the specific tool with the same
name.
2
By “document engineering process” I mean the act of editing interrelated documents in a
targeted way — similar to software engineering; see, e.g., www.documentengineering.org.
2
1.1 What Can You Use CDET for?
3
means to determine whether a set of formulae has a model, i.e., all formulae can
be fulfilled at once. Essentially, CDET is a sophisticated model checker, where
the DMS/RCS provides the model. We call a violation of a consistency rule
inconsistency. We can resolve an inconsistency by applying a repair to some
documents in the repository.
Consistency rules can express intra- and inter-document requirements regardless of the document model and the document format used. Strong rules must
be adhered to, whereas weak rules may be violated. Rules can restrict how documents evolve in time — hence, CDET supports temporal logic. From consistency
rules, CDET generates
• S-DAGs (S uggestion carrying D irected Acyclic Graphs), which visualize inconsistencies and repair actions for individual rules; and
• one repair collection, containing alternative repair sets, which each contains
repairs that together resolve all inconsistencies for all your rules.
1.1
What Can You Use CDET for?
Of course, you can use CDET for maintaining semantic consistency requirements
in a tolerant way during your document engineering projects. Besides pure consistency management, there are some other application areas:
• You can use temporal consistency rules for supervising and enforcing development processes.
• You can categorize documents on how they conform to some consistency
rules.
• You can even burn your CPU by CDET.
1.2
What is CDET not Meant for?
At date, CDET is in a very preliminary state — I consider it α software. Interfaces
to DMS/RCS are quite stable — so CDET should not corrupt your data. However,
I would not recommend CDET for mission critical tasks in high budgeted enterprise
projects. Sure, I am confident this changes in the near future. CDET is not
meant to ensure data integrity, locking, or to implement access rights; this should
be implemented by the DMS/RCS you are using. CDET does not take off the
responsibility to think about semantic consistency — in fact, it strongly encourages
such thoughts. Worse, you cannot use CDET for cooking coffee (except by using
the heat produced by your CPU) or carrying out your garbage . . .
4
1.3
Introduction
System Requirements & Installation
CDET has been tested on two Debian Linux boxes; it should run on other Linux/Unix boxes as well, may be you need to modify some paths. If you were
successful in running CDET, please let me know. CDET should be portable to
Windows without major efforts; however, I did not come around to that already.
For running CDET, you need the Glasgow Haskell Compiler (GHC) version 6.4 or
above, autoconf, and a DMS/RCS, including the headers of their support libraries.
Currently, CDET supports DARCS [Rou05], subversion [CSFP04], and the normal
file system.
For installing CDET, just grab the tar ball and unpack it. In the src subdirectory you should invoke
autoconf
which creates the configure script. For compiling CDET with file system support
only, simply type
./configure
for darcs support add the option --enable-darcs=<darcs_dir> (where <darcs_dir>
is the directory of your darcs sources); for subversion support add the option
--enable-svn. By typing
./configure --help
you can see a list of all available options. The configure script shows a short
summary of the CDET compile options. Now a simple
make
should compile CDET. By
make install
you copy CDET into your /usr/local/bin directory.
1.4
This Manual
From here, this manual proceeds as follows. In Chapter 2 you get to know CDET
from the author perspective by a small example. Chapter 3 shows details about
CDET’s system architecture. Chapter 4 is directed to the people who formalize
consistency requirements; here, you learn what you should provide CDET with
in order to get meaningful output. Chapter 5 includes a detailed description of
CDET’s syntax in a rather technical manner. Finally, in Chapter 6 lists some todo
items for future works. If you think some of these tasks is well suited to you or
you have other suggestions, please let me know — I will be happy to hear.
This is a manual only. Explaining formal details and algorithms behind CDET
is out of scope. You might want to look up such details in the research papers around CDET [SBRS03a, SBRS03b, SBRS04b, SSBS04, SBRS04c, SBRS04a,
SBBS05]. Notice that report generation as described in [SBRS03a, SBRS03b,
SBRS04b, SSBS04] is slightly out of date, though the general ideas still hold. If
you prefer the whole story as one large volume, see my PhD thesis [Sch04].
Chapter 2
Working with CDET
In this chapter you learn how to use the command line interface of CDET. Currently, there is no GUI support; so some of the interactive features are still not
accessible. This chapter is meant for authors, who do not need to know the formal
details about rules etc. Chapter 3 introduces the rˆole model of CDET.
For illustration, we assume a (ridiculously simple) toy example, which is also
used in some of my papers.
Example 2.1 Suppose you archive manuals over a long period of time. Documents (and manuals) reference manuals through keys (see Fig. 2.1). Since names
and kinds of manuals may change over time, you need key resolvers mapping keys
to their semantics, i.e., manual kind and name. Multiple key resolvers may exist.
Their actual names are hidden from authors. To ensure consistency, we require
that (two-step) links to manuals are valid (φ1 ) and names and kinds of manuals
are invariant over time (φ2 ). A link to a key k is valid if k is defined in a key
resolver and this definition points to an existing manual of the correct kind.
Fig. 2.1 also shows a repository that contains a plain text document doc1.txt
and three XML documents: a key resolver keys.xml, and two manuals man1.xml
and man2.xml. The check-in at state 2 causes three inconsistencies: (1) the reference to kaA3 violates φ1 because the kind of man1.xml is different from the kind
of kaA3’s key definition; (2) the reference to kaA2 violates φ1 because the key
key
documents
kind+
key resolvers
name
key
manuals
State 1 doc1.txt ...as shown in manual kaA3 ...
keys.xml <kDef key="kaA3"
kId="man1.xml"
kKind="technical M."/>
man1.xml <man kind="technical M."> ...
man2.xml <man kind="field M."> ...
State 2 doc1.txt ...as shown in kaA3 and kaA2 ...
man1.xml <man kind="field M."> ...
Figure 2.1: Example repository
5
6
Working with CDET
resolver does not contain a definition for kaA2; (3) the state transition violates φ2
because the kind of man1.xml has changed.
2
Suppose, we have already formalized the rules φ1 and φ2 as consistency rules.
Then do a
cdet --compile example_project.xml
in order to compile and optimize our rules, where example_project.xml contains
the project description of our example document engineering project.1 Rule compilation includes type checking; thus, it may fail if your rules include type errors.
Technically speaking, rule compilation creates some Haskell files and compiles
them via GHC. Finally, a new project-specific binary is compiled, say cdetExProj
for example. For large projects, compilation via GHC may take some time; so be
prepared to have some coffee at hand. You have to recompile the rules whenever
you change them.
After compilation, you can check your repository for consistency. Either you
can do this offline by issuing2
cdetExProj --check example_project.xml
or by including the above line in a so-called pre-commit hook script, in order to
check consistency online at each check-in. Using DARCS, you issue
darcs setpref test "cdetExProj --check example_project.xml"
at the command line (make sure you are in your DARCS repository). Of course,
you can edit the preferences file of your DARCS repository directly, see the DARCS
manual [Rou05] for further instructions. Currently, for subversion some strange
problems with the transaction mechanism currently prevent online consistency
checking.
Notice that during consistency checking in online mode, the repository is locked;
during consistency checking in offline mode, the repository is free for check-ins.
Consistency checking generates an S-DAG for each consistency rule. You can
“display” the S-DAGs on the text console doing a
cdetExProj --show example_project.xml [<repository state>]
The optional argument <repository state> can be used to display the S-DAGs
for this repository state only. For example, cdetExProj --show example_project.xml 2
displays the S-DAGs for the second repository state.
S-DAGs visualize inconsistencies and possible repair actions. The structure of
an S-DAG resembles that of a consistency rule. Nodes represent logical connectives
or atomic formulae; edges target the subformulae of a connective. We find inner
∃ universal quantifiers ,
∀ conjunctions ,
∧ and
nodes for existential quantifiers ,
∨ Leafs represent predicates, i.e., atomic formulae.
disjunctions .
Edges below quantifier nodes carry bindings of variables to values. A predicate
node occurs as a leaf only. It contains an atomic formula φ responsible for an
inconsistency and the truth value of φ.
∀ represents inconsistencies reFrom the user perspective, a universal node sulting from failure prone document content, where each edge blames a value for
∃
inconsistencies represented by the edge’s target S-DAG. An existential node 1
For each project, you need a project description, which imports the consistency rules and
sets some options.
2
Don’t worry about the path to the actual repository — it is included in the project description.
7
t 2
S−DAG for
rule φ 1
x {dId = doc1.txt, dState = 2}
k kaA2
d
k kaA3
= kaA3, kId = man1.xml,
{key
{
kKind = technical M.
False: k = key(d)
{
d
m
m
*
{k [kaA2
kaA3] 1},
{d.key [kaA3
kaA2] 5}
{
= kaA3, kId = man1.xml,{
{key
kKind = technical M.
= man1.xml, dState = 2,
{
{dId
kind = field M.
False: kind(m) = kKind(d)
Abandoned
{{m.kind [field M.
t2 2
S−DAG for
rule φ 2
technical M.] 2}}
t1 1
Abandoned
m2
*
m1
= man1.xml, dState = 1,
{
{dId
kind = technical M.
m2
= man1.xml, dState = 2,
{
{dId
kind = field M.
Abandoned
False: kind(m 1 ) = kind(m 2 )
{{m2.kind [field M.
technical M.] 2}}
Figure 2.2: Example S-DAGs
represents an inconsistency resulting from missing document content. This content could be either really missing or it could be regarded as missing because one
∧ and universal
of the edges carries defective content. Below conjunction nodes ∀ each S-DAG must be repaired. In contrast, it is sufficient to repair only
nodes ∨ and existential node ,
∃ respectively.
one S-DAG below a disjunction node At state 2 CDET generates the S-DAGs shown in Fig. 2.2. In the leaves
you find atomic formulae responsible for inconsistencies. At the edges below
quantifier nodes you find values blamed for inconsistencies. Let us read the SDAG for φ1 from its root to the leaves. At the second repository state (t 7→ 2)
you have an inconsistent document doc1.txt in your repository (x 7→ {dId =
doc1.txt, dState = 2}). Notice that CDET identifies a document by its name
dId and check-in state dState. The document doc1.txt contains two inconsistent
key references (k 7→ kaA2 and k 7→ kaA3). Let us first follow the left hand edge.
The key reference to kaA2 is inconsistent because the repository does not include
an appropriate key definition. You only have a key definition for the key kaA3
(d 7→ {key 7→ kaA3, . . .}). The left hand leaf indicates that the referenced key k is
different from the defined key key(d), which is due to the above bindings. Next,
we follow the right hand edge for k’s universal node. Here CDET finds a matching
key definition, which is the same as above. There is also a manual man1.xml in
the repository that looks promising (m 7→ {dId = man1.xml, dState = 2, . . .}).
This manual causes, however, an inconsistency because its kind (kind(m)) is different from the kind of the key definition (kKind(d)). This is indicated by the
Working with CDET
8
t 2
KEEP
S−DAG for
rule φ 1
Chg
x {dId = doc1.txt, dState = 2}
Del {dId = doc1.txt, dState = 2}
k kaA3 Del kaA3
kaA3 k kaA2
= kaA3, kId = man1.xml,
{key
{
kKind = technical M.
Chg key = kaA2, kId = man1.xml,
{kKind = technical M.
{
d
False: k = key(d)
{
= kaA3, kId = man1.xml,{
{key
kKind = technical M.
d
m
= man1.xml, dState = 2,
{
{dId
kind = field M.
Chg dId=man1.xml, dState = 2,
{ kind = technical M.
{
m
*
{k [kaA2
kaA3] 1},
{d.key [kaA3
kaA2] 5}
{
False: kind(m) = kKind(d)
Abandoned
{{m.kind [field M.
S−DAG for
rule φ 2
t2 2
t1 1
KEEP
KEEP
m1
Abandoned
m2
*
Abandoned
m2
technical M.] 2}}
= man1.xml, dState = 1,
{
{dId
kind = technical M.
KEEP
dId = man1.xml, dState = 2,
kind = field M.
Chg dId=man1.xml, dState = 2,
kind = technical M.
{
{
{
{
False: kind(m 1 ) = kind(m 2 )
{{m2.kind [field M.
technical M.] 2}}
Figure 2.3: Example augmented S-DAGs
right hand leaf. Sure, the repository contains a second manual man2.xml, which
would, however, cause more efforts for repair! S-DAGs will contain repairs that
impose minimal changes to the repository and preserve check-ins if possible. CDET
denotes S-DAGs that are not worth repairing by a special leaf Abandoned .
The S-DAG in Fig. 2.2 lacks concrete repair actions, i.e., to add, change,
or delete document content. In order to support interactive repair, CDET can
augment S-DAGs by repair actions after consistency checking. Simply issue
cdetExProj --augment example_project.xml [<repository state>]
at the command line. By the optional argument <repository state> you can
choose the repository state for which the S-DAGs should be augmented. If this
argument is not given, augmented S-DAGs contain repairs for all repository states.
During S-DAG augmentation, the repository is not accessed (and, therefore, not
locked).
Fig. 2.3 shows the augmented S-DAGs for the repository state 2; you can
view them by another cdetExProj --show example_project.xml. In addition,
cdetExProj --augment generates quite nice SVG pictures, which you can view
with your favorite WWW browser, and a structured XML output of the S-DAGs.
The name of the SVG picture is φ1 _SDAG.xml.svg for rule φ1 and φ2 _SDAG.xml.svg
for rule φ2 , respectively. You find these files in a directory given in the project
description file. Fig. 2.4 shows the generated SVG files. They look a bit different
from the ideal S-DAGs because currently, CDET’s implementation does not use
9
Figure 2.4: Example generated SVG files
Working with CDET
10
sophisitcated graph drawing algorithms. I expect this to change in the near future. In the SVG graphics each node is identified by a unique number that may
be referenced. In the S-DAG for φ1 you find the lower right leaf labeled Ref -> 6
— its incoming edge actually points to the node labeled by the number 6, which
you find on the left hand side. For efficiency reasons, S-DAGs are not fully shared.
In an augmented S-DAG, quantifier edges carry repair actions marked grey. An
action proposes to either add a value to (Add), or change a value within (Chg), or
delete a value from the sphere of this quantifier (Del). An action KEEP indicates
that the value must not be changed. For our example, CDET proposes to change
the key reference kaA2 to kaA3 or to delete the document doc1.txt. From an
augmented S-DAG you can choose repair actions interactively. CDET applies a
chosen repair action to an S-DAG. Since CDET’s current implementation lacks a
graphical user interface, this feature is not available at date, i.e., it is implemented
but you cannot access it.
Notice that, still, it is unclear which repair actions in an S-DAG must be applied
together in order to resolve all inconsistencies. You can instruct CDET to generate
the repair collection for both consistency rules, thus:
cdetExProj --derive example_project.xml [<repository state>]
By the optional argument <repository state> you can choose the repository
state for which the repair collection should be derived. But notice that the augmented S-DAGs must include this state, otherwise you will get an empty repair
collection. If this argument is not given, the repair collection will contain repairs
that derive all inconsistencies at all repository states (which is probably not what
you want).3 During repair derivation, the repository is not accessed (and, therefore, not locked). In contrast to S-DAG augmentation, you will notice that repair
derivation can take a long time because of the combinatorial explosion of repair
alternatives. CDET tries to reduce them but it cannot succeed in all cases.
The repair collection contains alternative repair sets, each including repairs that
are necessary and sufficient to repair all inconsistencies in the repository. CDET
guarantees that repairs within each set do not contradict each other and altogether
resolve the inconsistencies. Repairs may, however, introduce new inconsistencies.
Fig. 2.5 shows some repairs derived from our example S-DAGs at state 2. The
first component of a repair constitutes its sphere, the second component denotes
the proposed action. For example, the repair repk affects the variable k in the
rule φ1 . The repair proposes to change the key kaA2 into kaA3 in the document
doc1.txt at repository state 2. The repair resolves one inconsistency for a high
priority rule, may violate rule φ1 , and costs 1.4
The repair collection below shows how the repairs in Fig. 2.5 are best combined
in order to resolve all inconsistencies at state 2.


1.) {repk , repm,m2 }




2.) {repd , repm,m2 }


 3.) {repkaA2 , repm,m2 } 
4.) {repdoc1 , repm2 }
3
4
Also derivation will need plenty of time.
Repairs are rated by a simple cost model, based on natural numbers.
11
repk
= Rep {φ1 (k)}
refs(x)
{t 7→ 2, x 7→ {dId = doc1.txt, dState = 2}}
Chg kaA2
kaA3
Rate {1 (high)} {φ1 } 1
repd
= Rep {φ1 (d)}
concatMap(t, kDefs, repResDs(t))
{t 7→ 2}
Chg {key = kaA3, . . .}.key
kaA2
Rate {1 (high)} {φ1 } 5
repkaA2 = Rep {φ1 (k)}
refs(x)
{t 7→ 2, x 7→ {dId = doc1.txt, dState = 2}}
Del kaA2
Rate {1 (high)} {φ1 } 0
repdoc1 = Rep {φ1 (k)}
repDs(t)
{t 7→ 2}
Del {dId = doc1.txt, dState = 2}
Rate {3 (high)} {φ1 } 0
repm2
= Rep {φ2 (m2 )}
repManDs(t2 )
Chg {dId = man1.xml, . . .}.kind
Rate {1 (medium)} {φ1 , φ2 } 2
{t2 7→ 2}
technical M.
repManDs(t)
{t 7→ 2}
repm,m2 = Rep {φ1 (m), φ2 (m2 )}
Chg {dId = man1.xml, . . .}.kind
technical M.
Rate {2 (medium), 1 (medium)} {φ1 , φ2 } 2
Figure 2.5: Repairs generated for the rules φ1 and φ2
The collection implies a preference between the repair sets. In the example, you
change a document rather than deleting it. Changing a text document is preferred
to changing a key definition within a key resolver. In addition, you prefer deleting
some content within a document to deleting a whole document. Of course, you
can define your own preferences.
Chapter 3
CDET System Architecture
Fig. 3.1 illustrates the architecture of CDET. CDET distinguishes four rˆoles: authors, the project manager, the rule designer, and the language designer.
Authors use the DMS/RCS as usual, except if you formalize strong rules (see
below).
For specific projects, the project manager chooses consistency rules. In addition, he defines the ordering metrics for sorting the repair collection and global
options like the repository and the repository type, e.g., DARCS or subversion.
The rule designer formalizes consistency rules and hints, using a variant of
predicate logic. Rules define what consistency means — they reflect wishes from
an “administrator” perspective. CDET distinguishes between strong rules, which
must be adhered to, and weak rules, which may be violated. Hints guide repair
generation. In addition, the rule designer creates templates for documents. These
will be DTDs or Schemas, if XML is used as document format.
At a consistency check, CDET generates an S-DAG for each consistency rule.
CDET augments S-DAGs at request. From an augmented S-DAG authors can
choose repairs and apply them to the documents in the repository. Alternatively,
CDET can derive one ordered repair collection from all S-DAGs. The metrics for
sorting the collection is defined by the project manager.
Consistency rules use functions and predicates from domain-specific languages.
This makes the rules independent of concrete document formats, which can be
changed without affecting rules. During compilation, CDET checks consistency
rules for well-typedness w.r.t. the functions and predicates used. For convenience,
CDET provides a basic language Prelude, which defines fundamental functions,
predicates, and types.
In user-defined languages a language designer defines domain-specific functions, predicates, and types. The semantics of functions and predicates is defined
in Haskell [PJ03] — a statically typed purely functional programming language.
Haskell provides access to other libraries via a foreign function interface [C+ 03].
Such libraries offer sophisticated functionality, e.g., for parsing documents or
heuristics for semantic content analysis. Formal document types (usually corresponding to document templates) can be expressed by record or variant types.
This makes CDET independent of any particular document format and facilitates
12
13
access
external libs
(XPath, heuristics, ...)
Haskell
annotated
predicate logic
implemented
language
functions
types
predicates
language
designer
partly
derived
formalized
use & type check
consistency
rules & hints
document
rule templates
designer
project
manager
choose
project
templates
cdet −−compile
project
rules & hints
instance of
documents
author
choose
& apply
check in
consistency
check
cdetPrj
−−check
check out
repository
(managed by DMS/RCS)
S−DAGs
1.) repair set
2.) repair set
...
cdetPrj −−derive
augmented
S−DAGs
cdetPrj −−augment
Figure 3.1: CDET System Architecture (ovals mark fixed components; rectangles
mark customizable components)
heterogeneous repositories. If XML is used as document format, document types
and parser functions can be derived from DTDs, e.g., via HaXml [WR99].1
1
CDET uses an adapted version of HaXml that handles PackedStrings instead of normal
Strings.
Chapter 4
What You need to Input into
CDET?
In this chapter we explore the means you need for managing consistency for our
example, namely a project description, the consistency rules, and a language.
CDET’s current implementation uses XML for the concrete syntax. Also, you have
to edit these XML files by yourself; I plan, however, to develop some graphical
tools for this purpose. Using a DTD-aware XML editor (like emacs) already
alleviates editing XML files. This chapter is not meant for authors; they are not
confronted by the formal issues described here. This chapter is meant for rule
designers and language designers, who are experts in first-order logic and Haskell,
respectively. Due to the early prototype implementation, some things will appear
a bit complicated to you. I am sure that this will change in the future as CDET
evolves.
For our example project, suppose you have the following directory structure:
darcs/
dtd/
out/
haskell/
xml/
4.1
contains the DARCS repository you use for managing documents
contains two DTDs:
manual.dtd for manuals, resolver.dtd for key resolvers
here you will find the output of CDET (S-DAGs and repairs)
is your temporal directory for CDET; here the project-specific
binary is placed after compilation. Also the directory contains
a subdirectory cache
contains three XML files (project description, rules, language)
CDET Project Description
Let us first review the project manager ’s task. CDET uses the project description
as the entry point to your project; each project should have its own project description. For clarity, I do not recommend sharing project descriptions across projects
(in contrast to rules and languages). For our example, we use the following project
description file ManualsCheck.xml (located in the subdirectory xml/):
14
4.1 CDET Project Description
15
<consistencycheck name="Manuals"
reportdtd="../../../src/dtd/report.dtd"
tmpdir="../haskell/"
outputdir="../out/"
repositorybase="../darcs/"
repositorytype="darcs">
<performance usecache="true"
fastprelude="true"
incremental="true"
filterrules="true"
optimizerules="true"/>
<repair partialResolution="false" maxsets="10">
<metrics><![CDATA[
-- sum metrics
repairMetrics rs1 rs2
= sum (map rat rs1) >= sum (map rat rs2)
where rat rep = changeRat rep
+ offendsRat rep
+ costRat rep
-- punish deletion
changeRat rep = case change rep of
ActDelete v -> if isDocVal v ||
isDocListVal v
then -15 else -10
_ -> 0
-- punish offending rules
offendsRat rep = - (length (offends (rating rep)))
-- costs of a repair
costRat rep = case repaircost (rating rep) of
Just c -> -c
Nothing -> 0
]]></metrics>
</repair>
<!-- here are the CDET sources -->
<cdetdir path="../../../src"/>
<!-- import these rules -->
<importrules path="ManualsRules.xml"/>
</consistencycheck>
Let us take a closer look at the XML elements above:
<consistencycheck name="Manuals"
reportdtd="../../../src/dtd/report.dtd"
tmpdir="../haskell/"
outputdir="../out/"
repositorybase="../darcs/"
repositorytype="darcs">
First, we say that our project is called Manuals. The DTD for the consistency report produced by CDET can be found in the directory ../../../src/dtd/ and is
called report.dtd. You can use relative or absolute paths as you like. The temporal directory for CDET is ../haskell/. Here CDET also places the project-specific
16
What You need to Input into CDET?
binary after a successful cdet --compile; you may, however, copy the projectspecific binary whereever you like. CDET places its generated XML files in the
directory ../out/. There you will find (after appropriate commands) for each rule
φ its S-DAG structure (file name φ_SDAG.xml), the corresponding SVG file (file
name φ_SDAG.xml.svg), and the overall repairs (file name overallRepairs.xml).
The darcs repository holding our project documents is located in the directory
../darcs/.
<performance usecache="true"
fastprelude="true"
incremental="true"
filterrules="true"
optimizerules="true"/>
Above, you find performance options. I recommend to turn all performance options on, i.e., true. For our project, we use the internal caches of CDET (for
each function or predicate you can specify whether it should be cached). By
fastprelude you tell CDET to evaluate Prelude functions and predicates internally. The basic language Prelude contains large part of Haskell’s Prelude, see
App. A. We use incremental evaluation and only check those rules that might
be touched by a check-in. In addition, we let CDET optimize our rules, which
essentially means to push quantifiers into the rules.
<repair partialResolution="false" maxsets="10">
<metrics><![CDATA[
-- sum metrics
repairMetrics rs1 rs2
= sum (map rat rs1) >= sum (map rat rs2)
where rat rep = changeRat rep
+ offendsRat rep
+ costRat rep
-- punish deletion
changeRat rep = case change rep of
ActDelete v -> if isDocVal v ||
isDocListVal v
then -15 else -10
_ -> 0
-- punish offending rules
offendsRat rep = - (length (offends (rating rep)))
-- costs of a repair
costRat rep = case repaircost (rating rep) of
Just c -> -c
Nothing -> 0
]]></metrics>
</repair>
Above, we have specified options for repair generation. We turn off partial inconsistency resolution, which essentially means to generate a smaller repair collection.
The repair collection will contain at most 10 alternative repair sets. In the metric
element you find the Haskell code of the metric used to sort the repair collection.1
The above metric counts potentially violated rules (negatively) and subtracts the
repair cost, where deleting document content is punished by subtracting 10 and
1
Notice the use of <![CDATA[ in order to avoid XML parsing errors in the Haskell code.
4.2 Consistency Rules
17
deleting a document is punished by subtracting 15. In general, the punishment
of deletion should be greater than the cost of the most expensive hint. In fact,
deleting content (or even a whole document) is a fall-back solution that should be
considered only if no other repair is possible.
Technically, a metric is a Haskell function
repairMetrics :: [Repair] -> [Repair] -> Bool
that indicates whether we prefer the first list of repairs over the second list (for
simplicity, a repair list represents one alternative repair set). For defining metrics
you can use the following Haskell data types:
data Repair = Repair {vars :: [(Id,VSym)],
(rule identifiers and)
(variables x therein to repair)
ident :: (Id,Int), (unique identifier for a repair)
(original rule, unique number (for this rule))
domain :: Term,
(the term identifying the domain of x)
assign :: [(VSym,Value)],
(variable assignment for the domain)
change :: RepairAction, (the actual repair action)
rating :: Rating}
(rating for the repair)
data RepairAction =
ActDel Value
(delete value)
| ActChange Value Value
(change value from to)
| ActChangeField Value FSym Value
(change a field in a value)
| ActAdd Value
(insert value)
| ActChangeSuchThat PSym [Value] Bool
(we do not know how to set the value)
data Rating = Rating {offends :: [Id],
(possibly impacted rules)
resolves :: [(Int,Int)],
(how many inconsistencies resolved at which importance level)
repaircost :: Maybe Cost}
(repair costs)
In addition, isDocVal :: Value -> Bool determines whether a value is a document; isDocListVal :: Value -> Bool determines whether a value is a list
containing documents.
<!-- here are the CDET sources -->
<cdetdir path="../../../src"/>
<!-- import these rules -->
<importrules path="ManualsRules.xml"/>
Finally, we tell CDET about its own sources and import some rule sets. You can
specify as many rule sets as you like. ManualsRules.xml is also located in the
xml/ subdirectory and contains our example consistency rules.
4.2
Consistency Rules
We now go deeper into the formalization of consistency rules — the rule designer ’s
task. First, we explain how rules are formalized using the syntax of predicate logic.
Second, we show our example rules in CDET’s XML syntax.
18
What You need to Input into CDET?
φ1 Always links must be valid : At each state t, we have for all documents x at t,
that for all their referenced keys k there exists a key definition d (in one of the
resolvers) for k and there exists a manual m with name and kind as defined by d.
∀ tKEEP ∈ repStates • ∀ x ∈ repDs(t) • ∀ k ∈ refs(x) •
∃ d ∈ concatMap(kDefs, repResDs(t))
• ∃ m ∈ repManDs(t)
•
{k ; key(d) False 1 },
k = key(d)
{d.key ; k False 5}
∧
dId(m) = kId(d)
{{m.dId ; kId(d) False 3}}
∧
kind(m) = kKind(d)
{{m.kind ; kKind(d) False 2}}
φ2 Names and kinds of manuals are invariant over time: At all states t1 we have
for all manuals m1 at t1 that at all future states t2 there exists a manual m2 that
has the same name and the same kind as m1 .
KEEP
∀ tKEEP
∈ repStates • ∀ t2
∈ repStates •
1
¬
(t
≤
t
)
∨
1
2


∀ mKEEP
∈ repManDs(t1 ) • ∃ m2 ∈ repManDs(t2 ) •
1
 dId(m1 ) = dId(m2 )
{{m2 .dId ; dId(m1 ) False 3}} 


∧

kind(m1 ) = kind(m2 ) {{m2 .kind ; kind(m1 ) False 2}}
Figure 4.1: Example rules φ1 and φ2 with hints
Consistency rules are statements about repository states.2 The rule designer
formalizes consistency rules in a variant of temporal logic, based on the logic
proposed in [AHV96]. Instead of temporal operators like since or until, explicit
quantification over repository states is used in rules. Consistency rules mostly
correspond to standard first-order formulae, where the domain of a quantifier is
described by a term. As usual, rules use functions and predicates, which are
defined in languages (see Sect. 4.3).
For our example we define two rules as shown in Fig. 4.1. For clarity, we deal
with hint annotations (given in curly braces) later in this section.
Rule φ1 first quantifies over all repository states, provided by repStates;
repDs(t) returns the current documents for a state t. For each document x, the
variable k comprises the referenced keys, computed via refs(x). Key definitions in
the resolvers are determined with the help of the higher-order function concatMap.
It applies kDefs to each key resolver, computed by repResDs(t). Applied to a key
resolver, kDefs returns a list of key definitions, which are finally concatenated.
Thus, d ranges over the key definitions from all key resolvers; we require that
the referenced key k equals the key defined by d. The variable m ranges over all
manuals at the state t, computed by repManDs(t). The name of the manual m
must equal the name d points to, and the kind of m must equal the kind d points
to. Rule φ2 twice quantifies over time because two different versions of a manual
have to be related: the old version at state t1 and the new version at state t2 .
Repair generation requires domain-specific guidance because CDET supports
arbitrary predicates. For example, if an atomic formula p(x, y) is violated, CDET
2
A state represents a repository snapshot at a given time.
4.2 Consistency Rules
19
cannot anticipate how to change x and y in order to fulfill p(x, y). Therefore,
rule designers may annotate an atomic formula by a collection of hints, containing
alternative hint sets. Within a hint set, all hints are evaluated simultaneously.
Formally, a hint x ; e b c proposes to change the variable x to the term e if the
atomic formula evaluates to the truth value b; the repair imposes the cost c. If
the type of x is a record type, the hint x.f ; e b c proposes to change the field f
of x.
In order to repair a violated atomic formula k = key(d) in rule φ1 , the hints in
Fig. 4.1 propose to either change k to key(d) or change the field key of d to k. The
former repair imposes a cost of 1; the latter repair costs 5. We consider changing a
key definition more expensive because this might cause new inconsistencies regarding other referenced keys. In fact, the latter repair will be preferred if changing a
single key definition resolves multiple inconsistencies that could alternatively be
resolved by changing multiple manuals; in the above case changing a single key
definition is cheaper than changing six manuals. Notice that in φ1 the manuals
are “blamed” for inconsistent manual identifiers and kinds; the hints affect the
variable m only. A quantifier annotation tKEEP prevents S-DAG generation from
considering any repairs for the variable t. Of course, we cannot change repository
states, nor can we change old manual versions m1 .
Let us now formalize rule φ1 in CDET’s concrete XML syntax. Recall that for
our example we imported the rules from the file ManualsRules.xml, which starts
as follows:
<rules>
<importlanguage path="../../prelude/RulePrelude.xml"/>
<importlanguage path="ManualsLanguage.xml"/>
For formalizing rules, we use two languages: The predefined language Prelude
(defined in the file RulePrelude.xml) contains useful basic types, functions, and
predicates like Document, concatMap, and = (see App. A). The domain-specific
language in ManualsLanguage.xml contains some types and functions, specific for
our example project, e.g., a document type and a parser function for manuals.
<rule id="phi1" date="2004-08-16">
<meta weight="70" weak="true">
<desc>The two-step links to manuals are valid</desc>
</meta>
A rule starts with some meta data, e.g., its name (here phi1) and its definition
date (here 16 August 2004). We also assign the weight 70 to φ1 and tell CDET
that our example rule may be violated (weak="true"). If we prohibited violations,
CDET would not permit any check-ins to the repository that violate φ1 .
The actual formula begins with the tag <formula>. Let us now express the
quantifier cascade for the variables t, x, k, d, and m
∀ tKEEP ∈ repStates • ∀ x ∈ repDs(t) • ∀ k ∈ refs(x) •
∃ d ∈ concatMap(kDefs, repResDs(t)) • ∃ m ∈ repManDs(t) •
in XML:
20
What You need to Input into CDET?
<formula>
<forall action="keep" id="t">
<term>
<fapply id="repStates"/>
</term>
<formula>
<forall id="x">
<term>
<fapply id="repDs">
<term>
<var id="t"/>
</term>
</fapply>
</term>
<formula>
<forall id="k">
<term>
<fapply id="refs">
<term>
<var id="x"/>
</term>
</fapply>
</term>
<formula>
<exists id="d">
<term>
<fapply id="concatMap">
<term>
<sym id="kDefs"/>
</term>
<term>
<fapply id="repResDs">
<term>
<var id="t"/>
</term>
</fapply>
</term>
</fapply>
</term>
<formula>
<exists id="m">
<term>
<fapply id="repManDs">
<term>
<var id="t"/>
</term>
</fapply>
</term>
We express universal quantification by forall and existential quantification by
exists. Both elements carry the mandatory attribute id denoting the quanti-
4.2 Consistency Rules
21
fied variable and the optional attribute action denoting a quantifier annotation.
Immediately after the quantification tag we use the element term to denote the
quantifier sphere term. There fapply denotes the application of a function to
argument terms and var denotes a variable. Both elements carry the mandatory
attribute id denoting the function name and variable name, respectively. By sym
we denote an un-applied function that serves as a parameter to a higher-order
functions, e.g., <sym id="kDefs"/>. The subformula of a quantification is introduced by another formula element.
Let us concentrate on the three-way conjunction below the existential quantifier
for m:
k = key(d)
∧
dId(m) = kId(d)
∧
kind(m) = kKind(d)
{k ; key(d) False 1 },
{d.key ; k False 5}
{{m.dId ; kId(d) False 3}}
{{m.kind ; kKind(d) False 2}}
In CDET’s XML syntax we use and for conjunctions and or for disjunctions, where
both tags can carry arbitrarily many subformulae:
<formula>
<and>
<formula>
<papply id="==">
<term>
<var id="k"/>
</term>
<term>
<fapply id="key">
<term>
<var id="d"/>
</term>
</fapply>
</term>
<hintalternative>
<set condition="false" id="d" field="key" repaircost="5">
<term><var id="k"/></term>
</set>
</hintalternative>
<hintalternative>
<set condition="false" id="k" repaircost="1">
<term><fapply id="key">
<term><var id="d"/></term>
</fapply>
</term>
</set>
</hintalternative>
</papply>
</formula>
<formula>
<papply id="==">
<term>
22
What You need to Input into CDET?
<fapply id="dId">
<term>
<var id="m"/>
</term>
</fapply>
</term>
<term>
<fapply id="kId">
<term>
<var id="d"/>
</term>
</fapply>
</term>
<hintalternative>
<set condition="false" id="m" field="dId" repaircost="3">
<term><fapply id="kId">
<term><var id="d"/></term>
</fapply></term>
</set>
</hintalternative>
</papply>
</formula>
<formula>
<papply id="==">
<term>
<fapply id="kind">
<term>
<var id="m"/>
</term>
</fapply>
</term>
<term>
<fapply id="kKind">
<term>
<var id="d"/>
</term>
</fapply>
</term>
<hintalternative>
<set condition="false" id="m" field="kind" repaircost="2">
<term><fapply id="kKind">
<term><var id="d"/></term>
</fapply></term>
</set>
</hintalternative>
</papply>
</formula>
</and>
</formula>
Predicate application via papply corresponds to function application. A predicate application can carry alternative hint sets hintalternative, each of which
may include arbitrarily many hints (element set). Within the element set, the
4.3 Languages
23
attribute condition denotes the truth value of the predicate application that
should be inverted; id denotes the variable to change; field denotes the record
field to change (if appropriate); repaircost denotes the cost for repair. The set
element carries an arbitrary term that calculates the new value for the variable
(attribute id above).
Finally, we close all open tags:
</and>
</formula>
</exists>
</formula>
</exists>
</formula>
</forall>
</formula>
</forall>
</formula>
</forall>
</formula>
<actions/>
</rule>
<!-- rule phi2 omitted for brevity -->
</rules>
4.3
Languages
Our example rules use some symbols that are not defined yet, e.g., the symbol
“=” or the symbol “repStates.” These symbols are defined in languages. For
convenience, CDET provides the predefined language Prelude, which defines many
useful types and symbols (see App A).3 Therefore, you only need to define a
few symbols and types for specific projects. In this section we first review our
example language in a formal abstract syntax. Second, we explore the concrete
XML syntax, which again will be a bit more verbose.
For our example we define the language ManualsLanguage, which contains
symbols and types as shown in Fig. 4.2. ManualsLanguage imports the predefined language Prelude, the relevant part of which is also shown in Fig. 4.2. For
simplicity, our formalism neglects import relations between languages. We let <
denote an explicit subtype relation between record types; a record type may have
multiple supertypes.
The variant list type [α] is declared as usual in functional programming [MTH90,
PJ03]; the variant constructors are [] (empty list) and (:) (add an element to the
front of a list). The record type Document stands for a formal document, carrying
a name (of type String) and a check-in state (of type State). That way we distinguish different document versions. CDET requires that each document type is
a subtype of Document. This is important for efficient consistency checking. The
record type ResD resembles the key resolver structure (see Fig. 2.1 on pg. 5). ResD
inherits all record labels from its supertype Document. Our notion of subtyping
3
Roughly, Prelude defines large part of Haskell’s Prelude, hence the name.
24
What You need to Input into CDET?
Extract from language Prelude (predefined)
Type definitions
String
[α]
=
[] | (:) α×[α]
Document = Document {dId : String, dState : State}
Predicate symbol definitions
=
: ∀α.α×α → Bool
≤
: ∀α.α×α → Bool
<
: ∀α.α×α → Bool
Function symbol definitions
concatMap : ∀α, β.(α → [β])×[α] → [β]
repStates : [State]
strings
Haskell like lists
documents
equality
less than or equal
less than
Haskell like concatMap
all repository states
Language ManualsLanguage, defined by the language designer (imports Prelude)
Type definitions
ManD < {Document} = Man {kind : String} manual documents
ResD < {Document} = Res {kDefs : [KDef]} key resolver documents
KDef
= KDef {key : String, kId : String, kKind : String}
key definitions
Function symbol definitions
repDs
: State → [Document] get all documents in the repository
repManDs
: State → [ManD]
get all manual documents
repResDs
: State → [ResD]
get all resolver documents
refs
: Document → [String] keys referenced in a document
Figure 4.2: Example types and symbols (the operator : separates a symbol from
its type, → separates the argument types of a function type or predicate type from
the result type, × separates argument types)
resembles XML Schema subtyping via extension and restriction [W3C01]. Record
and variant type definitions induce new function symbols (labels and constructors,
respectively). For example, ResD induces kDefs : ResD → [Item].
We regard predicate symbols as function symbols with a boolean result type,
denoted by Bool. Function symbols starting with rep provide access to documents
within the repository at a given state. For a document d, refs(d) returns all
referenced keys. concatMap(f, xs) applies the function f to each member of the
list xs and concatenates the result lists. Record labels can serve as parameter
for concatMap, e.g., in concatMap(kDefs, repResDs(t)). In addition, we have to
define the semantics of the symbols in our new ManualsLanguage; still no one
tells CDET what the symbols really do. For semantics definition, CDET employs
Haskell.
Let us define our ManualsLanguage in CDET’s concrete XML syntax. Recall that we have imported the file ManualsLanguage.xml in our rule definition.
ManualsLanguage.xml starts as follows:
<language id="ManualsLanguage">
<importlanguage path="../../prelude/RulePrelude.xml" qualifiedAs="P"/>
<importparser dtd="../dtd/manual.dtd" qualifiedAs="Man"/>
<importparser dtd="../dtd/resolver.dtd" qualifiedAs="Res"/>
4.3 Languages
25
Above, we import the basic language Prelude such that we can define our new
symbols and types in terms of functions and types defined in Prelude. In addition,
we generate two parsers for manuals and resolver documents from their DTDs.
CDET uses an HaXml [WR99] adaptation for generating appropriate Haskell types
and parsers. Unfortunately, these Haskell types do not exactly correspond to the
Haskell types generated by CDET, because HaXml lacks support for subtyping.
Thus, there will be still some work to do; but at least you do not have to struggle
with lexing and parsing issues . . . We import the generated parsers qualified in
order to avoid naming conflicts.
Next, we define our three new record types
Type definitions
ManD < {Document} = Man {kind : String} manual documents
ResD < {Document} = Res {kDefs : [KDef]} key resolver documents
KDef
= KDef {key : String, kId : String, kKind : String}
key definitions
in XML
<typedefs>
<typedef id="ManD">
<desc>Manual document</desc>
<record rcon="ManD">
<supers>
<gtype>
<tapply tcref="Document"/>
</gtype>
</supers>
<label id="kind" key="false">
<gtype>
<tapply tcref="PString"/>
</gtype>
</label>
</record>
</typedef>
<typedef id="ResD">
<desc>Resolver document</desc>
<record rcon="ResD">
<supers>
<gtype>
<tapply tcref="Document"/>
</gtype>
</supers>
<label id="kDefs" key="false">
<gtype>
<tapply tcref="[]">
<gtype>
<tapply tcref="KDef">
</tapply>
</gtype>
</tapply>
</gtype>
</label>
What You need to Input into CDET?
26
</record>
</typedef>
<typedef id="KDef">
<desc>Key definition</desc>
<record rcon="KDef">
<supers/>
<label id="key" key="true">
<gtype>
<tapply tcref="PString"/>
</gtype>
</label>
<label id="kId" key="true">
<gtype>
<tapply tcref="PString"/>
</gtype>
</label>
<label id="kKind" key="true">
<gtype>
<tapply tcref="PString"/>
</gtype>
</label>
</record>
</typedef>
</typedefs>
For a record type we specify a record constructor, which may be different from the
type constructor (as in Haskell). The supertypes of a record type are given by the
supers element. The element gtype denotes a ground type (i.e., a non-function
type); tapply denotes the application of a type constructor to ground types. For
example,
<gtype>
<tapply tcref="[]">
<gtype>
<tapply tcref="KDef">
</tapply>
</gtype>
</tapply>
</gtype>
means to apply the type constructor [] to the type KDef, which we would write
[] KDef or, more commonly, [KDef] in Haskell. After the record’s supertypes,
we specify the record labels. The label element carries an optional key attribute.
CDET compares record values by inspecting their key labels only. So, by specifying only a few key labels, you can speed up comparisons (and thus consistency
checking) significantly. But you must guarantee that records are distinguishable
by their key labels only, otherwise you get rather strange results! For document
types (i.e., subtypes of Document) it is safe to make all record labels non key labels
because the repository guarantees that given a repository state and a document
name, we find at most one document in the repository.
You might wonder about the type PString. For efficiency reasons CDET
uses an array based String type, in contrast to Haskell (where Strings are lists
of Characters). Internally, CDET uses the FastPacketString library from the
DARCS [Rou05] distribution.
4.3 Languages
27
Since we do not define new predicate symbols, we include
<predsymdefs/>
and go on with the definition of our first function symbol
repDs : State → [Document] get all documents in the repository
in XML:
<funsymdefs>
<funsymdef id="repDs">
<desc>Documents in the repository</desc>
<meta>
<docdep regex="./*.xml"/>
<docdep regex="./*.txt"/>
<cachemeta cached="true" reftrans="true">
<argdep num="0"/>
</cachemeta>
</meta>
<funtype>
<type>
<gtype>
<state/>
</gtype>
</type>
<gtype>
<tapply tcref="[]">
<gtype>
<tapply tcref="Document"/>
</gtype>
</tapply>
</gtype>
</funtype>
<code>
repDs repo t = ds
where ds=repDocs "./*.xml" t repo ++
repDocs "./*.txt" t repo
</code>
</funsymdef>
Above, we have defined the new function symbol repDs, which accesses the documents ending with *.xml or *.txt. The symbol is referentially transparent and
CDET should cache the symbol results in order to improve performance. In addition, the symbol result depends on its first argument (CDET starts counting by
zero) only. Referential transparency and annotations of accessed documents are
essential for efficient consistency checking. I plan to implement some syntactic
analysis that automatically retrieves these information out of the symbol’s source
code: for the moment, however, you have to provide these annotations by your
own.
After the symbol metadata we define the symbol type. Above, we say that
the argument type is State; the result type is a list of documents. The funtype
element denotes a function type consisting of some argument types and a result
type. The type element comprises both function types and ground types (element
What You need to Input into CDET?
28
gtype). A function type must always result in a ground type in order to ensure
the first-order properties of CDET’s logic.
Finally, we define the semantics of the symbol repDs by giving its Haskell source
code. The first argument of each function and predicate is the repository (which
is an abstract Haskell data type). Notice that this argument is implicit, i.e., it is
not part of the type declaration. Above, we simply retrieve some documents from
the repository with help of the repository access function
repDocs :: String -> State -> Repository -> [Document]
The first argument denotes a regular file pattern as you know it from your dayto-day work with files. Essentially, a regular file pattern is a regular expression
where the dot (“.”) is not escaped explicitly.
That was easy, wasn’t it. Let us look at the function repManDs, which should
return the manuals
repManDs : State → [ManD] get all manual documents
In CDET’s XML syntax we write:
<funsymdef id="repManDs">
<desc>Manuals in the repository</desc>
<meta>
<docdep regex="./man*.xml"/>
<cachemeta cached="true" reftrans="true">
<argdep num="0"/>
</cachemeta>
</meta>
<funtype>
<type>
<gtype>
<state/>
</gtype>
</type>
<gtype>
<tapply tcref="[]">
<gtype>
<tapply tcref="ManD"/>
</gtype>
</tapply>
</gtype>
</funtype>
<code>
repManDs repo t
= map (\ d -> mkMan d $ fromJust’ (err d) $ fromJust’ (err d) $
parseDoc d repo readXml) ds
where err d = "repManDs: internal error reading xml " ++ show d
ds=repDocs "./man*.xml" t repo
mkMan :: Document -> Man.Man -> ManD
mkMan d (Man.Man attrs _)
= ManD {manD_dId = document_dId d,
manD_dState = document_dState d,
manD_kind = Man.manKind attrs}
fromJust’ err (Just a) = a
4.3 Languages
29
fromJust’ err Nothing = error err
</code>
</funsymdef>
The Haskell source above looks a bit more complicated because we have to parse
manuals. Their names and check-in states are not sufficient; we need their structure. For accessing documents in the repository, you can use the repository access
function
parseDoc :: Document -> Repository -> (String -> a) -> Maybe a
It gets the document to parse, the repository, and a parser function as arguments.4
parseDoc retrieves the document from the repository and applies the parser function to its content (given as String). The parser function should convert the
document content into some data structure, which is returned if the document
exists. For convenience, CDET provides a standard parser for XML documents,
which is generated by HaXml automatically. Recall that we told CDET to do this
for manuals and key resolvers in the language header! Technically, CDET’s HaXml
generates an instance for the type class XmlContent, which provides the function
readXml :: (XmlContent a) => String -> Maybe a.
Unfortunately, Haskell and HaXml both lack subtyping support, such that
the types generated by HaXml and by CDET, respectively, are not compatible.5
HaXml generates the following types for manuals from the DTD manuals.dtd
(you can view them in the generated Haskell module haskell/DTD_manual.hs):6
data Man = Man Man_Attrs PackedString
deriving (Eq,Show)
data Man_Attrs = Man_Attrs
{ manKind :: PackedString
} deriving (Eq,Show)
CDET generates the following type for manuals from our language definition (you
can view them in the generated Haskell module haskell/ManualsLanguageTypes.hs):
data ManD = ManD {
manD_dId :: PString,
manD_dState :: State,
manD_kind :: PString}
deriving (Eq, Ord)
In Haskell CDET’s general document type looks as follows:
data Document = Document {
document_dId :: PString,
document_dState :: State}
deriving (Eq, Ord)
For bridging these types, we have defined the helper function mkMan above. I
admit that this is the most complex task in the work with CDET. But you have
to do this only once.
Let us risk a look at the definition of the function repResDs:
repResDs : State → [ResD] get all resolver documents
Here we have to bridge the following HaXml types (you can find them in the file
haskell/DTD_resolver.hs):
4
You might ask at what repository state the document is accessed — its the check-in state of
the document given as first argument.
5
I plan to overcome this severe shortcoming by a HaXml extension that supports a subset of
XML Schema and subtypes.
6
Notice that PString is just a type synonym for PackedString.
30
What You need to Input into CDET?
newtype Res = Res [KDef] deriving (Eq,Show)
data KDef = KDef KDef_Attrs Descr
deriving (Eq,Show)
data KDef_Attrs = KDef_Attrs
{ kDefKey :: PackedString
, kDefKId :: PackedString
, kDefKKind :: PackedString
} deriving (Eq,Show)
newtype Descr = Descr PackedString deriving (Eq,Show)
to the CDET types (also in haskell/ManualsLanguageTypes.hs)
data ResD = ResD {
resD_dId :: PString,
resD_dState :: State,
resD_kDefs :: [KDef]}
deriving (Eq, Ord)
data KDef = KDef {
kDef_kId :: PString,
kDef_kKind :: PString,
kDef_key :: PString}
deriving (Eq, Ord)
We do this by the function mkResD below.
<funsymdef id="repResDs">
<desc>resolver documents in the repository</desc>
<meta>
<docdep regex="./key*.xml"/>
<cachemeta cached="true" reftrans="true">
<argdep num="0"/>
</cachemeta>
</meta>
<funtype>
<type>
<gtype>
<state/>
</gtype>
</type>
<gtype>
<tapply tcref="[]">
<gtype>
<tapply tcref="ResD"/>
</gtype>
</tapply>
</gtype>
</funtype>
<code>
repResDs repo t
= map (\ d -> mkResD d $ fromJust’ (err d) $ fromJust’ (err d) $
parseDoc d repo readXml) ds
where err d = "repResD: internl error reading xml" ++ show d
ds=repDocs "./key*.xml" t repo
mkResD :: Document -> Res.Res -> ResD
mkResD d (Res.Res kdefs)
= ResD {resD_dId = document_dId d,
resD_dState = document_dState d,
4.3 Languages
31
resD_kDefs = map mkKDef kdefs}
mkKDef (Res.KDef attrs _)
= KDef {kDef_key = Res.kDefKey attrs,
kDef_kId = Res.kDefKId attrs,
kDef_kKind = Res.kDefKKind attrs}
</code>
</funsymdef>
What is left is the function refs, which scans an arbitrary document for referenced
keys.
refs : Document → [String] keys referenced in a document
Below, we tell CDET that a key begins with the letters kaA and is separated from
other text by white spaces. Sure, you can imagine more complex definitions than
the one below:
<funsymdef id="refs">
<desc>Key references inside a document.</desc>
<meta>
<docargdep num="0"/>
<cachemeta cached="true" reftrans="true">
<argdep num="0"/>
</cachemeta>
</meta>
<funtype>
<type>
<gtype>
<tapply tcref="Document"/>
</gtype>
</type>
<gtype>
<tapply tcref="[]">
<gtype>
<tapply tcref="PString"/>
</gtype>
</tapply>
</gtype>
</funtype>
<code>
refs repo d = fromJust’ (err d) (parseDoc d repo getRefs)
where err d = "refs: internal error reading document " ++ show d
getRefs :: String -> [PString]
getRefs content = map packString $ filter isKeyRef (words content)
isKeyRef w = keyprefix == (take 3 w)
keyprefix = "kaA"
</code>
</funsymdef>
</funsymdefs>
</language>
That’s it, you have defined your first CDET language.
Sure, defining languages suffers from poor tool support. In the future, I will
particularly focus on the gap between HaXml and CDET’s subtypes. When this
gap is closed, language definition will be almost as easy as rule formalization.
Chapter 5
Technical Details
In this chapter we take a deep technical look at the XML syntax of CDET, i.e., the
project description syntax, the language definition syntax, and the rule definition
syntax. For the S-DAG XML syntax and the repair collection syntax see the report
DTD in App. B.4. The syntax descriptions below directly correspond to XML
elements. Finally, in Sect. 5.4 we present CDET’s generic repository interface.
We present the grammars in “DTD tree style.” You find the child elements of
an element e below e and slightly indented. An element may be annotated by ?
(element is optional), * (element may appear arbitrarily often), + (element must
appear at least once), ++ (element must appear at least twice). If not otherwise
noted, the order of subelements is significant. An element description may be
omitted if the element was described before or will be described below.
5.1
Project Description XML Syntax
• consistencycheck
The configuration of your project
Required attributes: name (the name of your project), tmpdir (the temporal directory for CDET), outputdir (the output directory for CDET),
reportdtd (the DTD for consistency reports), repositorybase (the base
directory of your repository), repositorytype (your DMS/RCS, currently
supported are dir, darcs, and subversion)
– performance
Performance options
Required attributes: usecache (use CDET’s internal caches?), fastprelude
(use internal computation for Prelude functions?), incremental (check
consistency incrementally?), filterrules (only check rules influenced
by a check-in?), optimizerules (rewrite rules for faster consistency
checking?)
– repair
Options for repair
Required attributes: partialResolution (should we permit partial inconsistency resolution?)
Optional attributes: maxsets (maximum number of alternative repair
sets)
32
5.2 Language XML Syntax
33
∗ metrics?
The metrics for sorting the repair sets. Here you
can place a Haskell implementation of the function
repairMetrics :: [Repair] -> [Repair] -> Bool
– cdetdir
The CDET source directory.
Required attributes: path (the directory path)
– includedir*
Extra include directories needed to compile your
project, e.g., directories from which you import parsers or auxiliary
Haskell modules.
Required attributes: path (the directory path)
– importrules+
One or more rule sets for your project. Against
the rules from these files your repository will be checked for consistency.
Required attributes: path (the rule definition file)
5.2
Language XML Syntax
language
A user defined language, needed by some rules. A language defines types, predicate symbols, and function symbols.
Required attributes: id (the name of the language, use a unique name, different
from any other language, project description, or rule set)
Implied attributes: qualifiedPrelude (import Prelude qualified with this name),
qualifiedChar (import Char qualified with this name), qualifiedRatio (import Ratio qualified with this name), qualifiedComplex (import Complex qualified with this name), qualifiedNumeric (import Numeric qualified with this
name), qualifiedIx (import Ix qualified with this name), qualifiedList (import List qualified with this name), qualifiedMaybe (import Maybe qualified
with this name), qualifiedRandom (import Random qualified with this name),
qualifiedTime (import Time qualified with this name)
By default, the Haskell Prelude is imported unqualified; the other Haskell modules are imported fully qualified.
• desc?
A comprehensive description for your language.
• importlanguage*
Import another language such that you can use
symbols of the imported language for symbol definition.
Required attributes: path (the XML file holding the imported language)
Optional attributes: qualifiedAs (qualified import with a given name)
• importmodule*
Import an auxiliary Haskell module.
Required attributes: module (the name of the Haskell module)
Optional attributes: qualifiedAs (qualified import with a given name)
• importparser*
Generate and import a parser for a given DTD. The
parser will be generated by HaXml.
Required attributes: dtd (the name of the DTD for which the Parser should
be generated)
Optional attributes: qualifiedAs (qualified import with a given name)
34
Technical Details
• importforeign*
Import a foreign function, say from a C library (currently, only C is supported)
Required attributes: call (calling convention, currently ccall only), header
(the C header file), foreign (the name of the foreign function), haskell (the
name of the corresponding Haskell function)
The following subelements specify the type of the Haskell function. You
need extra XML elements for this in order to prevent XML parsing errors.
– fargtype*
Argument types of the imported function’s Haskell
side.
Required attributes: id (the argument type name)
– frestype
The result type of the imported function’s Haskell side.
Required attributes: id (the result type name)
• typedefs
The type definitions of the language. You may define as
many types as you want. Notice, however, that their names must be unique.
– typedef*
A type definition, which can be either atomic, record,
or variant.
Required attributes: id (the type constructor name)
∗ desc?
A comprehensive description of the type.
One of the following type definitions is permitted:
∗ atomic
An atomic type like Int or Char.
∗ record
A record type like Document.
Required attributes: rcon (the record constructor, not to be confused with the record type constructor although often the same)
· tvar*
Type variables (arguments) for the record type.
Required attributes: id (the type variable name)
· supers?
Supertypes of the defined type. You can specify
multiple supertypes by the subelement
gtype*
(see below)
Any type variables in a gtype element must be arguments of
the record type (tvar above).
· label*
The labels of the record type. Here you specify
the record type’s ingredients.
Required attributes: id (the name of the label)
Optional attributes: key (is the label a key label?). For testing
equality, key labels are considered only! If the attribute is
omitted, CDET assumes (for safety reasons) that the label is a
key label.
By the subelement
gtype
you specify the label’s type (see below).
∗ variant
A variant type like Bool.
· tvar*
Type variables (arguments) for the variant type.
Required attributes: id (the type variable name)
5.2 Language XML Syntax
35
· subs?
Subtypes of the defined variant type. You can
specify multiple subtypes by the subelement
gtype*
(see below)
Any type variables in a gtype element must be arguments of
the variant type (tvar above).
· vcon*
The variant data constructors.
Required attributes: id (the variant constructor name)
If the variant constructor has type arguments, you can specify
them by the subelement
gtype*
Again, any type variables in a gtype element must be arguments of the variant type (tvar above).
• predsymdefs
Predicate symbol definitions. You can define as many
predicate symbols as you want. Notice, however, that their names must be
unique.
– predsymdef*
A predicate symbol definition.
Required attributes: id (the predicate symbol name)
∗ desc?
A comprehensive description of the predicate symbol.
∗ meta?
Predicate symbol metadata.
Optional attributes: calcStates (does the symbol calculate over
repository states?) If the attribute is not given, CDET is optimistic
and assumes that the symbol does not calculate over repository
states.
· docdep*
Document dependencies.
Required attributes: regex: List here a pattern of files, the
predicate symbol directly accesses via a repository access function. I hope to calculate these patterns in the future.
· docargdep*
Argument dependencies of a symbol.
Required attributes: num: Give here the argument number, responsible for document access. I hope to calculate these numbers in the future.
· cachemeta
Additional metadata to influence caching behavior.
Required attributes: cached (should the symbol be cached?),
reftrans (is the symbol referentially transparent, i.e., does it
not use repStates or repHead?)
In general, Haskell guarantees referential transparency of each
symbol. The repository access functions repStates or repHead
can, however, change their result between consistency checks.
By the subelement
argdep*
you specify the argument numbers, the result of the predicate
symbol depends on. Usually, these are all argument numbers,
but sometimes not.
36
Technical Details
∗ predtype
The predicate type. You need to specify the argument types only because each predicate has a boolean result type.
· type*
low).
Argument types of the predicate symbol (see be-
∗ code
Finally, the Haskell code of the predicate symbol’s implementation. The first parameter of each symbol is the repository
(type Repository). Otherwise you could not access the repository.
Then follow the parameters as specified by the predicate symbol’s
type above. Don’t forget to enclose the code by a CDATA section in
order to avoid XML parsing errors.
• funsymdefs
Function symbol definitions. You can define as many
function symbols as you want. Notice, however, that their names must be
unique.
– funsymdef*
A function symbol definition.
Required attributes: id (the function symbol name)
∗ desc?
A comprehensive description of the function symbol.
∗ meta?
Function symbol metadata (see above).
∗ funtype
The function symbol’s type, consisting of (general)
argument types and a ground result type.
· type*
Argument types, which can be either ground types
(gtype) or function types (funtype). This supports the definition of higher-order functions, which result in a non-function
type. This restriction is necessary to keep CDET’s logic first
order.
One of the following subelements is supported.
gtype
(ground type)
funtype
(function type)
· gtype
A ground type, i.e., a non-function type. Here,
the ground type is the result type of a function symbol.
A ground type can be either a type application (tapply), a type
variable (tvar), the supertype of all types (top), or the repository state type (state). Hence one of the following subelements is permitted:
tapply
(type constructor application)
The attribute tcref specifies the type constructor to apply.
The subelement
gtype*
specifies the argument types.
tvar
(type variable) The attribute id specifies the
type variable name.
top
(the supertype of all types)
state
(the repository state type)
∗ code
Finally, the Haskell code of the function symbol’s implementation. The first parameter of each symbol is the repository
5.3 Rule XML Syntax
37
(type Repository). Otherwise you could not access the repository.
Then follow the parameters as specified by the function symbol’s
type above. Don’t forget to enclose the code by a CDATA section in
order to avoid XML parsing errors.
5.3
Rule XML Syntax
rules
A user defined rule set. Here you define what consistency means.
You can import this rule set in a project description.
• importlanguage+
Import at least one language, the symbols of which
you use in your rules.
Required attributes: path (the XML file holding the imported language)
• importrule*
Import other rule sets. This implies that whenever this
rule set is used by a project, all other imported rule sets are used, too.
Required attributes: path (the XML file holding the imported rule set)
• rule*
A consistency rule.
Required attributes: id (the rule name, must be unique), date (the date of
the last rule modification)
– meta
Rule metadata.
Required attributes: weight (importance level of the rule), weak (may
the rule be violated?)
∗ desc?
A comprehensive description for this rule.
∗ docdeps?
Document dependencies. By these document dependencies you can override the dependencies calculated by CDET.
Sometimes the calculated dependencies are too pessimistic and you
know better. The more restrictive the document dependencies are
the more consistency checking is accelerated.
· docdep*
Document dependencies.
Required attributes: regex (pattern of files, the rule accesses)
– formula
The actual predicate logic formula, described below.
The formula element contains the predicate logic part of a rule, which is rather
standard. It consists of the following subelements.
• desc?
A comprehensive description of the formula. Here I plan to
include some automatic translation of the formula into natural language.
The formula itself may be one of the following (like in classic predicate logic):
• papply
An atomic formula, i.e., predicate symbol application to some
argument terms.
Required attributes: id: The predicate symbol to apply. Make sure that the
symbol is defined in a language imported by this rule set.
38
Technical Details
– term*
Argument terms of the predicate symbol application.
Make sure that the result types of the argument terms “fit” to the predicate symbol’s type (modulo polymorphism and subtyping of course).
CDET’s type checker will assist you in this.
A term consists of a comprehensive description and the actual term.
∗ desc?
A comprehensive description of the term. Here I plan
to include some automatic translation into natural language.
CDET’s notion of terms is a bit more expressive than in classic predicate logic. CDET supports variables, function symbol application,
function symbols as such, record construction, variant deconstruction, and explicitly typed terms (to guide type inference). A term
may be one of the following:
∗ var
A variable. Make sure that you only reference variables
that are bound by a quantifier; else you get a type error. CDET
supports closed formulae only.
∗ fapply
A function symbol application.
Required attributes: id: The function symbol to apply. Make sure
that the symbol is defined in a language imported by this rule set.
· term*
Argument terms of the function symbol application. Make sure that the result types of the argument terms
“fit” to the function symbol’s type (modulo polymorphism and
subtyping of course). CDET’s type checker will assist you in
this.
∗ sym
A function symbol as argument of a higher-order function.
Required attributes: id: The function symbol’s name. Make sure
that the symbol is defined in a language imported by this rule set.
∗ rec
A record construction.
Required attributes: id: The record data constructor, not to be
confused with the record type constructor. Make sure that the
record data constructor is defined in a language imported by this
rule set (and that it constructs the correct record type of course).
· label*
Label bindings for the record construction. Make
sure that you bind all labels of the record including those of
the record’s supertypes.
Required attributes: id: The record label’s name. Make sure
that the name is part of the record type and that you bind it
only once in a record construction.
The label is bound to a term, which you specify by the subelement
term
∗ case
A variant deconstruction.
Optional attributes: tcref: You may want to specify the variant
type constructor in case you construct variant supertypes without
adding new variant data constructors. Then CDET’s type checker
may need some guidance.
5.3 Rule XML Syntax
39
· term
The variant term to be deconstructed, i.e., the
case scrutinee.
· binding*
Bindings of each alternative variant data constructor (including those of the subtypes) to a function symbol,
which will be applied to the variant data constructor’s arguments.
Required attributes: id (the variant constructor, unique in the
case construct); sym (the function symbol that should be applied to the variant constructor’s arguments)
∗ typed
An explicitly typed term. Explicit typing may guide
type inference, which is, however, only seldom necessary.
· term
· type
The actual term.
It’s type annotation.
– hintalternative*
An alternative hint set. You can guide repair
generation by giving hints that tell CDET about how the truth values
of atomic formulae can be inverted.
∗ set*
A hint inside a hint set. All hints in a hint set are
executed simultaneously. Essentially, a hint tells CDET about how
a variable should be changed in order to invert the truth value of
the atomic formula at hand.
Required attributes: id (the variable to which the hint applies)
Optional attributes: condition: The truth value of the atomic formula responsible for executing the hint; this truth value should be
inverted. If the attribute is not given, CDET will execute the hint
on either truth value.
varcondition: Should the hint be executed if the variable is new
(content has changed since the last check-in) or old (content remained constant since the last check-in)? If the attribute is not
given, CDET will execute the hint always.
field: If the variable’s type is a record type you can specify the
record label to be changed. If the attribute is not given the hint
applies to the full value of the variable.
repaircost: You can specify the cost of the hint, in order to get
the cheapest repairs only. If the attribute is not given, nothing is
assumed about the cost — hence you might get more repair alternatives.
By the subelement
term
you tell CDET how the variable (or the field) should be changed.
Make sure that the term’s type corresponds to the variable’s type
(or the field’s type if given). Otherwise, you get a type error.
• or
Classical disjunction.
– formula++
two).
The disjunction’s subformulae (you need at least
40
Technical Details
• and
Classical conjunction.
– formula++
two).
• not
Classical negation.
– formula
• implies
The conjunction’s subformulae (you need at least
The negated subformula.
Classical implication.
– formula
The first argument formula of the implication (the one
that implies something).
– formula
The second argument formula of the implication (the
one that is implied).
• forall
Universal quantification.
Required attributes: id: The quantified variable. Make sure that within a
rule you quantify at most once over a variable. For clarity and simplicity,
CDET does not support multiple quantification over the same variable. Of
course in different rules you can “reuse” variables.
Optional attributes: action: Here you can specify a preferred repair action
for the quantified variable. The following actions are supported: delete
(only derive repairs to delete something), change (only derive repairs to
change something), keep (don’t derive any repairs for this variable).
keepdomain: Cache the quantifier domain (the values over which the quantifier iterates). Use this feature with caution since quantifier domains may
become really large.
– term
A term that tells CDET where the values of the bound
variable come from. Over all these values the quantifier iterates. Make
sure that the type of the term is a list [τ ]; then the quantified variable
has the type τ .
– formula
The argument formula; here the quantified variable is
“in scope” and may be referenced in terms.
• exists
Existential quantification (attributes and subelements are similar to those of universal quantification).
Required attributes: id: The quantified variable.
Optional attributes: action: Here you can specify a preferred repair action for the quantified variable. The following actions are supported: add
(only derive repairs to add something), change (only derive repairs to change
something), keep (don’t derive any repairs for this variable).
keepdomain: Cache the quantifier domain.
– term
A term that tells CDET where the values of the bound
variable come from.
– formula
The argument formula of the existential quantification;
here the quantified variable is “in scope.”
5.4 Repository Interface
5.4
41
Repository Interface
In this section you learn details about CDET’s generic interface to the repository of
an arbitrary DMS/RCS. As already mentioned, CDET only makes few assumptions
about the underlying DMS/RCS. The interface consists of five Haskell functions,
which you can use for implementing functions and predicates (the abstract Haskell
data type Repository represents the repository itself):
• repStates :: Repository -> [State] returns all states of a given repository.
• repHead :: Repository -> State returns the current repository state.
• repDocs :: Repository -> State -> String -> [Document] returns
the documents in the repository that are current at a given state and match
a regular expression. For example, repDocs repo 2 "*.xml" returns all
XML documents current at state 2 in the repository repo. Notice that the
returned documents only include the name and the last modification state
(up to the given state).
data Document = Document
{document_dId :: PString,
document_dState :: State}
The content of the document has to be parsed by the function parseDoc
described below.
• repDirs :: Repository -> State -> String -> [Folder] behaves like
repDocs but returns directories instead. Similar to documents, directories
include the name and the last modification state only.
data Folder
= Folder
{folder_fId :: PString,
folder_fState :: State}
• parseDoc :: Repository -> Document -> (String -> a) -> Maybe a
accesses a given document in the repository. The third parameter is a function that parses the document content and converts it into an appropriate
Haskell data structure. For XML documents, such parser functions can be
generated [WR99]. If the given document does not exist in the repository,
parseDoc returns Nothing.
Chapter 6
Future Work
As you might have noticed, CDET is far from being a mature product. Indeed,
CDET is in a very preliminary state. Here are just some directions for future work:
• Support type definition by a subset of XML Schema and derive parsers
automatically in a HaXml like manner.
• Improve incremental consistency checking for XML documents, provided
that the DMS/RCS supports XML patches.1 .
• Implement some graphical tools for rule formalization, language definition,
and S-DAG playing.
• Improve repairs by data mining approaches.
• Translate rules and repairs into natural language.
You feel that you could help in some of the above points? You want to add
something? You have an interesting document engineering project and want to apply CDET? Then feel free to contact me, e.g., by email [email protected].
1
see www.unibw.de/inf2/OO VCS/
42
Appendix A
The CDET Prelude
Here we list the basic CDET language Prelude, which includes large part of the Haskell prelude, helper functions from the FastPackedString library from the DARCS distribution,
and some basic repository access functions.
A.1
Prelude Types
For convenience we use infix notation where appropriate. Notice that in CDET’s XML
syntax you have to use prefix notation instead.
Haskell like Int
Haskell like Char
PackedString from DARCS
Haskell like Float
Haskell like Maybe
Haskell like Bool
Haskell like 2 tuples
Haskell like 3 tuples
tuples up to 7 tuples
[] | α : [α]
Haskell like lists
dId : PString,
Document Document
Documents (name and check-in state)
dState : State
Int
Char
PString
Float
Maybe α
Bool
(α, β)
(α, β, γ)
...
[α]
A.2
atomic
atomic
atomic
atomic
Just α | Nothing
True | False
(α, β)
(α, β, γ)
Prelude Predicates
Notice that in Haskell equality and inequality require the type class Eq. In contrast,
CDET lets GHC derive instances for the type class Eq for each type, such that equality
and inequality are fully polymorphic. The same holds for class members of the Haskell
type class Ord.
==
: α × α → Bool
fullEq : α × α → Bool
/=
: α × α → Bool
<
: α × α → Bool
<=
: α × α → Bool
>
: α × α → Bool
>=
: α × α → Bool
all
: (α → Bool) × [α] → Bool
any
: (α → Bool) × [α] → Bool
equality (key fields only)
full structural equality
inequality (key fields only)
less than
less than or equal
greater than
greater than or equal
Haskell like all
Haskell like any
43
The CDET Prelude
44
elem
: α × [α] → Bool
elemS : Char × PString → Bool
notElem : α × [α] → Bool
even
: Int → Bool
odd
: Int → Bool
null
: [α] → Bool
nullS : PString → Bool
and
: [Bool] → Bool
or
: [Bool] → Bool
A.3
Haskell like elem
elem for packed Strings
Haskell like notElem
Haskell like even
Haskell like odd
Haskell like null
null for packed Strings
Haskell like and
Haskell like or
Prelude Functions
Notice that CDET does not support constant values in formulae, such that we provide
some numerical constants as function symbols with no parameter. Notice further that
due to lack of type classes, CDET distinguishes functions for number calculations w.r.t.
their type Int or Float.
const0
: Int
const1
: Int
const2
: Int
id
:α→α
succInt : Int → Int
predInt : Int → Int
+Int
: Int × Int → Int
−Int
: Int × Int → Int
∗Int
: Int × Int → Int
/Int
: Int × Int → Int
absInt
: Int × Int → Int
mod
: Int × Int → Int
divMod
: Int × Int → (Int, Int)
succFloat : Float → Float
predFloat : Float → Float
+Float
: Float × Float → Float
−Float
: Float × Float → Float
∗Float
: Float × Float → Float
/Float
: Float × Float → Float
absFloat : Float × Float → Float
round
: Float → Int
floor
: Float → Int
ceiling : Float → Int
mkFloat : Int → Float
maximum : [α] → α
minimum : [α] → α
++
: [α] × [α] → [α]
appendS : PString × PString → PString
head
: [α] → α
headS
: PString → Char
last
: [α] → α
tail
: [α] → [α]
tailS
: PString → PString
0
1
2
Haskell like id
Haskell like succ for Int
Haskell like pred for Int
Haskell like + for Int
Haskell like - for Int
Haskell like * for Int
Haskell like div for Int
Haskell like abs for Int
Haskell like mod
Haskell like divMod
Haskell like succ for Float
Haskell like pred for Float
Haskell like + for Float
Haskell like - for Float
Haskell like * for Float
Haskell like / for Float
Haskell like abs for Float
Haskell like round
Haskell like floor
Haskell like ceiling
Convert an Int into a Float
Haskell like maximum
Haskell like minimum
Haskell like ++
++ for packed Strings
Haskell like head
head for packed Strings
Haskell like last
Haskell like tail
tail for packed Strings
A.3 Prelude Functions
init
: [α] → [α]
take
: Int × [α] → [α]
takeS
: Int × PString → PString
drop
: Int × [α] → [α]
dropS
: Int × PString → PString
reverse
: [α] → [α]
reverseS
: PString → PString
diff
: [α] × [α] → [α]
length
: [α] → Int
lengthS
: PString → Int
lookup
: α × [(α, β)] → Maybe β
!!
: [α] × Int → α
indexS
: PString × Int → Char
map
: (α → β) × [α] → [β]
concatMap
: (α → [β]) × [α] → [β]
foldl
: (α × β → α) × α × [β] → α
foldlS
: (α × Char → α) × α × PString → α
foldr
: (α × β → β) × β × [α] → β
foldrS
: (Char × β → β) × β × PString → β
filter
: (α → Bool) × [α] → [α]
filterElem
: [β] × (α → β) × [α] → [α]
filterNotElem : [β] × (α → β) × [α] → [α]
takeWhile
: (α → Bool) × [α] → [α]
takeWhileS
: (Char → Bool) × PString → PString
dropWhile
: (α → Bool) × [α] → [α]
dropWhileS
: (Char → Bool) × PString → PString
productInt
: [Int] → Int
sumInt
: [Int] → Int
productFloat : [Float] → Float
sumFloat
: [Float] → Float
splitAt
: Int × [α] → ([α], [α])
splitAtS
: Int × PString → (PString, PString)
span
: (α → Bool) × [α] → ([α], [α])
spanS
: (Char → Bool) × PString
:
→ (PString, PString)
break
: (α → Bool) × [α] → ([α], [α])
breakS
: (Char → Bool) × PString
:
→ (PString, PString)
fst
: (α, β) → α
snd
: (α, β) → β
maybe
: β × (α → β) × Maybe α → β
catMaybes
: [Maybe α] → [α]
zip
: [α] × [β] → [(α, β)]
zipWith
: (α × β → γ) × [α] × [β] → [γ]
unzip
: [(α, β)] → ([α], [β])
words
: [Char] → [[Char]]
lines
: [Char] → [[Char]]
wordsS
: PString → [PString]
linesS
: PString → [PString]
unwords
: [[Char]] → [Char]
45
Haskell like init
Haskell like take
take for packed Strings
Haskell like drop
drop for packed Strings
Haskell like reverse
reverse for packed Strings
Haskell like \ \
Haskell like length
length for packed Strings
Haskell like lookup
Haskell like !!
!! for packed Strings
Haskell like map
Haskell like concatMap
Haskell like foldl
foldl for packed Strings
Haskell like foldr
foldr for packed Strings
Haskell like filter
advanced filter
advanced negative filter
Haskell like takeWhile
takeWhile for packed Strings
Haskell like dropWhile
dropWhile for packed Strings
Haskell like product for Int
Haskell like sum for Int
Haskell like product for Float
Haskell like sum for Float
Haskell like splitAt
splitAt for packed Strings
Haskell like span
span for packed Strings
Haskell like break
break for packed Strings
Haskell like fst
Haskell like snd
Haskell like maybe
Haskell like catMaybes
Haskell like zip
Haskell like zipWith
Haskell like unzip
Haskell like words
Haskell like lines
words for packed String
lines for packed String
Haskell like unwords
The CDET Prelude
46
unlines : [[Char]] → [Char]
unwordsS : [PString] → PString
unlinesS : [PString] → PString
concat
: [[α]] → [α]
concatS : [PString] → PString
nilS
: PString
repStates : [State]
repHead : State
repInit : State
next
: State → State
prev
: State → State
prevState : State → State
Haskell like unlines
unwords for packed String
unlines for packed String
Haskell like concat
concat for packed Strings
empty packed String
all repository states
repository head state
initial repository state
next repository state
previous repository state
total version of prev
Appendix B
DTDs
Here you find the complete DTDs of CDET.
B.1
Project Description DTD consistencycheck.dtd
<!-- top level configuration element -->
<!ELEMENT consistencycheck (performance,repair,cdetdir,includedir*,importrules+)>
<!-- name: a name for your project -->
<!-- tmpdir: directory where temporal files can be stored -->
<!-- outputdir: directory where the generated XML files are stored -->
<!-- reportdtd: where is the DTD for the consistency report -->
<!-- repositorybase: base directory of your repository -->
<!-- repositoryconfig: optional configuration file for some repository types -->
<!-currently this is necessary for subversion only -->
<!-other repositories ignore this value -->
<!-- repositorytype: type of the repository (dir | darcs | subversion | cas) -->
<!ATTLIST consistencycheck
name CDATA #REQUIRED
tmpdir CDATA #REQUIRED
outputdir CDATA #REQUIRED
reportdtd CDATA #REQUIRED
repositorybase CDATA #REQUIRED
repositoryconfig CDATA #IMPLIED
repositorytype (dir | darcs | subversion | cas) #REQUIRED>
<!-- some performance tuning -->
<!-- you _should_ turn on everything -->
<!ELEMENT performance EMPTY>
<!-- usecache: should we use caches? -->
<!-- fastprelude: functions from Haskell’s Prelude
be evaluated internally? -->
<!-- incremental: generate S-DAGs incrementally? -->
<!-- filterrules: only check rules influenced by a check-in? -->
<!-- optimizerules: rewrite rules for optimum performance? -->
<!ATTLIST performance
47
48
DTDs
usecache (true | false) #REQUIRED
fastprelude (true | false) #REQUIRED
incremental (true | false) #REQUIRED
filterrules (true | false) #REQUIRED
optimizerules (true | false) #REQUIRED>
<!-- influence repair generation -->
<!ELEMENT repair (metrics?)>
<!-- maxalts: not supported at the moment! -->
<!-- partialResolution: support partial inconsistency resolution? -->
<!-- maxsets: maximum alternative repair sets in the repair collection -->
<!ATTLIST repair
maxalts CDATA #IMPLIED
partialResolution (true | false) #REQUIRED
maxsets CDATA #IMPLIED>
<!ELEMENT metrics (#PCDATA)>
<!-- user defined preference metrics to sort repair sets -->
<!-- function to be defined:
repairMetrics :: [Repair] -> [Repair] -> Bool -->
<!-- Types to be used: -->
<!-- data Repair = Repair {vars :: [(Id,VSym)], (rule identifiers and)
<!-(variables x therein to repair)
<!-ident :: (Id,Int), -->
<!-(unique identifier for a repair)
<!-(original rule, unique number (for this rule))
<!-domain :: Term,
(the term identifying the domain of x)
<!-assign :: [(VSym,Value)],
(variable assignment for the domain)
<!-(cannot contain x)
<!-change :: RepairAction,
(the actual repair action)
<!-rating :: Rating}
(rating for the repair)
<!-- data RepairAction = -->
<!-ActDel Value
(delete value)
<!-| ActChange Value Value
(change value from to)
<!-| ActChangeField Value FSym Value (change a field in a value)
<!-| ActInsert Value
(insert value)
<!-| ActChangeSuchThat PSym [Value] Bool -->
<!-(we do not know how to set the value)
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
-->
<!-- data Rating = Rating {offends :: [Id], (possibly impacted rules) -->
<!-resolves :: [(Int,Int)], -->
<!-(how many incons. resolved at which importance level) -->
<!-repaircost :: Maybe Cost
(repair costs)} -->
<!-- directory for the CDET sources for rule and language compilation -->
<!-- this is the parent directory of the "CDET" directory -->
<!ELEMENT cdetdir EMPTY>
B.2 Rules DTD rules.dtd
<!ATTLIST cdetdir
path CDATA #REQUIRED>
<!-- include cirectories needed for rule and language compilation -->
<!ELEMENT includedir EMPTY>
<!ATTLIST includedir
path CDATA #REQUIRED>
<!-- rulesets against which the repository should be checked -->
<!ELEMENT importrules EMPTY>
<!ATTLIST importrules
path CDATA #REQUIRED>
B.2
Rules DTD rules.dtd
<!-- top level ruleset element -->
<!ELEMENT rules (importlanguage+,importrule*,rule*)>
<!-- import a language -->
<!ELEMENT importlanguage EMPTY>
<!-- path to the XML file holding the language definition -->
<!ATTLIST importlanguage
path CDATA #REQUIRED>
<!-- import another ruleset -->
<!ELEMENT importrule EMPTY>
<!-- path to the XML file holding the ruleset definition -->
<!ATTLIST importrule
path CDATA #REQUIRED>
<!-- consistency rule -->
<!ELEMENT rule (meta,formula,actions)>
<!-- date: creation date of the rule -->
<!-if a rule is newer than the last runtime then
it might have been changed -->
<!-- id: rule identifier -->
<!ATTLIST rule
date CDATA #REQUIRED
id ID #REQUIRED> <!-- rule name -->
<!-- rule metadata -->
<!ELEMENT meta (desc?,precon*,docdeps?)>
<!-- weight: rule weight (importance) 0 .. 100 -->
<!-- weak: may a rule be violated? -->
<!ATTLIST meta
weight CDATA "0"
weak (true | false) #REQUIRED>
49
50
DTDs
<!-- consistency rule description -->
<!ELEMENT desc (#PCDATA)>
<!-- rule precondition: this rule must be satisfied in order to check -->
<!-- the current rule (not supported at the moment) -->
<!ELEMENT precon EMPTY>
<!ATTLIST precon
id CDATA #REQUIRED>
<!-- document dependencies of a rule -->
<!-- not given: dont know (determined by CDET) -->
<!-- given: these are the documents the rule really depends on -->
<!ELEMENT docdeps (docdep*)>
<!ELEMENT docdep EMPTY>
<!-- regex: regular expression of the dependent documents -->
<!ATTLIST docdep
regex CDATA #REQUIRED>
<!-- first order formula with description -->
<!ELEMENT formula
(desc?,(papply | or | and | not | implies | forall | exists))>
<!-- applied predicate (atomic formula) plus hint collection -->
<!ELEMENT papply (term*,hintalternative*)>
<!-- id: predicate symbol -->
<!ATTLIST papply
id CDATA #REQUIRED>
<!-- alternative hint set -->
<!ELEMENT hintalternative (set*)>
<!-- hint -->
<!ELEMENT set (term)>
<!-- condition: predicate result causing to execute the hint -->
<!-- id: variable to set -->
<!-- varcondition: set variable only if it is marked new / old -->
<!-- field: record field to set -->
<!-- repaircost: cost imposed by executing the corresponding repair -->
<!ATTLIST set
condition (true | false) #IMPLIED
id CDATA #REQUIRED
varcondition (new | old) #IMPLIED
field CDATA #IMPLIED
repaircost CDATA #IMPLIED>
<!-- disjunction -->
<!ELEMENT or (formula,formula+)>
<!-- conjunction -->
B.2 Rules DTD rules.dtd
51
<!ELEMENT and (formula,formula+)>
<!-- implication -->
<!ELEMENT implies (formula,formula)>
<!-- negation -->
<!ELEMENT not (formula)>
<!-- universal quantification with sphere term -->
<!ELEMENT forall (term,formula)>
<!-- id: quantified variable -->
<!-- action: hint for quantifier -->
<!-- keepdomain: also cache the quantifier sphere (may be expensive!) -->
<!ATTLIST forall
id CDATA #REQUIRED
action (delete | add | change | keep) #IMPLIED
keepdomain (true | false) #IMPLIED>
<!-- existential quantification with sphere term -->
<!ELEMENT exists (term,formula)>
<!-- id: quantified variable -->
<!-- action: hint for quantifier -->
<!-- keepdomain: also cache the quantifier sphere (may be expensive!) -->
<!ATTLIST exists
id CDATA #REQUIRED
action (delete | add | change | keep) #IMPLIED
keepdomain (true | false) #IMPLIED> <!-- quantified variable -->
<!-- TERMS -->
<!-- term with description -->
<!ELEMENT term (desc?,(var | fapply | sym | rec | case | typed))>
<!-- variable -->
<!ELEMENT var EMPTY>
<!-- id: variable name -->
<!ATTLIST var
id CDATA #REQUIRED>
<!-- applied function symbol -->
<!ELEMENT fapply (term*)>
<!-- id: function symbol name -->
<!ATTLIST fapply
id CDATA #REQUIRED>
<!-- function symbol e.g. as argument for higher order functions -->
<!ELEMENT sym EMPTY>
<!-- id: function symbol name -->
52
DTDs
<!ATTLIST sym
id CDATA #REQUIRED>
<!-- record construction -->
<!ELEMENT rec (label)*>
<!-- id: record constructor name -->
<!ATTLIST rec
id CDATA #REQUIRED>
<!-- record label -->
<!ELEMENT label (term)>
<!-- id: label name (unique for this record) -->
<!ATTLIST label
id CDATA #REQUIRED>
<!-- variant deconstruction -->
<!ELEMENT case (term,binding*)>
<!-- tcref: variant constructor (type constructor) -->
<!ATTLIST case
tcref CDATA #IMPLIED>
<!-- binding inside case: id -> sym -->
<!ELEMENT binding EMPTY>
<!-- id: variant constructor -->
<!-- sym: function symbol to be applied to constructor arguments -->
<!ATTLIST binding
id CDATA #REQUIRED
sym CDATA #REQUIRED>
<!-- explicitly typed term -->
<!ELEMENT typed (term,type)>
<!-- user defined action what should be done with the report -->
<!-- not supported at the moment -->
<!ELEMENT actions (mailreport*, mailrepair*,mailsummary?)>
<!-- Mail the report to some recipients -->
<!-- not supported at the moment -->
<!ELEMENT mailreport (recipient+)>
<!ATTLIST mailreport
currentonly (true | false) #REQUIRED
explain
(true | false) #REQUIRED
format
(xml | latex) #REQUIRED
attachDocs (true | false) #REQUIRED>
<!-- Mail the repair suggestions to some recipients -->
<!-- not supported at the moment -->
<!ELEMENT mailrepair (recipient+)>
B.3 Language DTD language.dtd
<!ATTLIST mailrepair
currentonly
explain
format
attachDocs
(true | false) #REQUIRED
(true | false) #REQUIRED
(xml | latex) #REQUIRED
(true | false) #REQUIRED>
<!-- Mail a comprehensive summary to some recipients -->
<!-- not supported at the moment -->
<!ELEMENT mailsummary (recipient+)>
<!ELEMENT recipient EMPTY>
<!ATTLIST recipient
mailto CDATA #REQUIRED>
<!-- TYPES -->
<!-- type: ground or function type -->
<!ELEMENT type (gtype | funtype)>
<!-- groundtype -->
<!ELEMENT gtype (tapply | tvar | top | state)>
<!-- type application -->
<!ELEMENT tapply (gtype*)>
<!-- tcref: type constructor to be applied -->
<!ATTLIST tapply
tcref CDATA #REQUIRED>
<!-- type variable -->
<!ELEMENT tvar EMPTY>
<!-- id: type variable name -->
<!ATTLIST tvar
id CDATA #REQUIRED>
<!-- supertype of all other types -->
<!ELEMENT top EMPTY>
<!-- repository state -->
<!ELEMENT state EMPTY>
<!-- function type -->
<!ELEMENT funtype (type*,gtype)>
B.3
Language DTD language.dtd
<!-- top level language element -->
<!ELEMENT language (desc?,importlanguage*,importmodule*,importparser*,
importforeign*,typedefs, predsymdefs, funsymdefs)>
<!-- id: language name -->
53
54
DTDs
<!-- qualifiedPrelude: import Haskell’s Prelude qualified as -->
<!-- qualifiedXMLTypes: import HaXml types qualified as (you should do that)-->
<!-- qualifiedChar: import Haskell’s Char module qualified as -->
<!-- qualifiedRatio: import Haskell’s Ratio module qualified as -->
<!-- qualifiedComplex: import Haskell’s Complex module qualified as -->
<!-- qualifiedNumeric: import Haskell’s Numeric module qualified as -->
<!-- qualifiedIx: import Haskell’s Ix module qualified as -->
<!-- qualifiedList: import Haskell’s List module qualified as -->
<!-- qualifiedMaybe: import Haskell’s Maybe module qualified as -->
<!-- qualifiedRandom: import Haskell’s Random module qualified as -->
<!-- qualifiedTime: import Haskell’s Time module qualified as -->
<!-- by default we import Prelude unqualified and -->
<!-all other modules fully qualified -->
<!ATTLIST language
id CDATA #REQUIRED
qualifiedPrelude CDATA #IMPLIED
qualifiedXMLTypes CDATA #IMPLIED
qualifiedChar CDATA #IMPLIED
qualifiedRatio CDATA #IMPLIED
qualifiedComplex CDATA #IMPLIED
qualifiedNumeric CDATA #IMPLIED
qualifiedIx CDATA #IMPLIED
qualifiedList CDATA #IMPLIED
qualifiedMaybe CDATA #IMPLIED
qualifiedRandom CDATA #IMPLIED
qualifiedTime CDATA #IMPLIED>
<!-- import other languages -->
<!ELEMENT importlanguage EMPTY>
<!-- path: path to the XML file holding he language -->
<!-- qualifiedAs: import qualified (default: unqualified import) -->
<!ATTLIST importlanguage
path CDATA #REQUIRED
qualifiedAs CDATA #IMPLIED>
<!-- import an XML parser automatically generated by HaXml for a DTD -->
<!ELEMENT importparser EMPTY>
<!-- dtd: path to the DTD -->
<!-- qualifiedAs: import name (necessary to avoid naming conflicts) -->
<!ATTLIST importparser
dtd CDATA #REQUIRED
qualifiedAs CDATA #REQUIRED>
<!-- import another Haskell module -->
<!ELEMENT importmodule EMPTY>
<!-- module: path to the Haskell module -->
<!-- qualifiedAs: import qualified (default: unqualified import) -->
<!ATTLIST importmodule
module CDATA #REQUIRED
qualifiedAs CDATA #IMPLIED>
B.3 Language DTD language.dtd
<!-- import a foreign function -->
<!-- currently only C is supported by GHC -->
<!ELEMENT importforeign (fargtype*,frestype)>
<!-- call: calling convention (currently ccall only) -->
<!-- header: the C header file (implies object file to link) -->
<!-- foreign: the name of the foreign function -->
<!-- haskell: the name of the corresponding haskell function -->
<!ATTLIST importforeign
call (ccall | cplusplus | dotnet | jvm | stdcall) #REQUIRED
header CDATA #REQUIRED
foreign CDATA #REQUIRED
haskell CDATA #REQUIRED>
<!-- an argument type of the corresponding haskell function -->
<!-- use an extra element here
to avoid XML parsing errors for Haskell’s arrow -->
<!ELEMENT fargtype EMPTY>
<!-- id: name of the argument type -->
<!ATTLIST fargtype
id CDATA #REQUIRED>
<!-- the result type of the corresponding haskell function -->
<!ELEMENT frestype EMPTY>
<!-- id: name of the result type -->
<!ATTLIST frestype
id CDATA #REQUIRED>
<!-- SYMBOL DEFINITIONS -->
<!-- function symbol definitions -->
<!ELEMENT funsymdefs (funsymdef)*>
<!-- function symbol definition -->
<!ELEMENT funsymdef (desc?,meta?,funtype,code)>
<!-- id: function symbol name -->
<!ATTLIST funsymdef
id CDATA #REQUIRED>
<!-- predicate symbol defintions -->
<!ELEMENT predsymdefs (predsymdef)*>
<!-- predicate symbol definition -->
<!ELEMENT predsymdef (desc?,meta?,predtype,code)>
<!-- id: predicate symbol name -->
<!ATTLIST predsymdef
id CDATA #REQUIRED>
55
56
DTDs
<!-- implementation of symbols (Haskell source code) -->
<!ELEMENT code (#PCDATA)>
<!-- SYMBOL METADATA for function and predicate symbols -->
<!-- description -->
<!ELEMENT desc (#PCDATA)>
<!-- detailed metadata -->
<!ELEMENT meta (docdep*,strdep*,docargdep*,cachemeta)>
<!-- calcStates: does the symbol calculate over repository states? -->
<!ATTLIST meta
calcStates (true | false) #IMPLIED>
<!-- document dependencies of the symbol -->
<!ELEMENT docdep EMPTY>
<!-- regex: regular expression of documents the result depends on -->
<!ATTLIST docdep
regex CDATA #REQUIRED>
<!-- string dependencies of the symbol -->
<!ELEMENT strdep EMPTY>
<!-- regex: regular expression of strings the may symbol result in -->
<!ATTLIST strdep
regex CDATA #REQUIRED>
<!-- document argument dependencies of the symbol -->
<!ELEMENT docargdep EMPTY>
<!-- num: argument number responsible for document access -->
<!ATTLIST docargdep
num CDATA #REQUIRED>
<!-- cache metadata for a symbol -->
<!ELEMENT cachemeta (argdep*,property*)>
<!-- cached: should the symbol be cached? -->
<!-- reftrans: is the symbol referentially transparent? -->
<!ATTLIST cachemeta
cached (true | false) #REQUIRED
reftrans (true | false) #REQUIRED>
<!-- argument dependencies of the symbol -->
<!ELEMENT argdep EMPTY>
<!-- num: argument number responsible for symbol result -->
<!ATTLIST argdep
num CDATA #REQUIRED>
<!-- symbol properties (not supported at the moment) -->
B.3 Language DTD language.dtd
57
<!ELEMENT property (simprop | fungenprop| predgenprop)>
<!-- simple property -->
<!ELEMENT simprop EMPTY>
<!-- prop: simple property: transitive, symmetric, antisymmetric,
asymmetric, reflexive, irreflexive -->
<!ATTLIST simprop
prop (trans | sym | antisym | asym | refl | irrefl) #REQUIRED>
<!-- generic properties for function symbols (currently not supported) -->
<!-- pre results imply post result -->
<!-- something similar to ghc rule pragmas -->
<!ELEMENT fungenprop (fpre*,fpost)>
<!-- pre-result: arguments and function result (all simple variables) -->
<!ELEMENT fpre (arg*)>
<!-- res: result variable -->
<!ATTLIST fpre
res CDATA #REQUIRED>
<!ELEMENT arg EMPTY>
<!-- arg: argument variable -->
<!ATTLIST arg
id CDATA #REQUIRED>
<!-- post result: arguments and function result -->
<!ELEMENT fpost (arg*)>
<!ATTLIST fpost
res CDATA #REQUIRED>
<!-- generic properties for predicate symbols -->
<!-- pre results imply post result -->
<!-- something similar to ghc rule pragmas -->
<!ELEMENT predgenprop (ppre*,ppost)>
<!ELEMENT ppre (arg*)>
<!ATTLIST ppre
res (true | false) #REQUIRED>
<!ELEMENT ppost (arg*)>
<!ATTLIST ppost
res (true | false) #REQUIRED>
<!-- TYPE DEFINITIONS -->
<!-- type definitions -->
<!ELEMENT typedefs (typedef)*>
<!-- type definition: atomic, record, variant -->
58
DTDs
<!ELEMENT typedef (desc?,(atomic|record|variant))>
<!-- id: type (constructor) name -->
<!ATTLIST typedef
id CDATA #REQUIRED>
<!-- atomic type like Int, Char -->
<!ELEMENT atomic EMPTY>
<!-- record type: argument type variables, super types, labels -->
<!-- only! argument tyvars can be used in definition -->
<!ELEMENT record (tvar*,supers?,label*)>
<!-- rcon: record constructor -->
<!ATTLIST record
rcon CDATA #REQUIRED>
<!-- super types of a record -->
<!ELEMENT supers (gtype*)>
<!-- record label -->
<!ELEMENT label (gtype)>
<!-- id: label name -->
<!-- key: the label belongs to the key of a record -->
<!-- records can be identified by _only_ looking at their key labels -->
<!-- only key labels are used for value comparison and in repairs -->
<!ATTLIST label
key (true | false) #IMPLIED
id CDATA #REQUIRED>
<!-- variant type: argument types, subtypes, constructors -->
<!ELEMENT variant (tvar*,subs?,vcon*)>
<!-- subtypes of a variant -->
<!ELEMENT subs (gtype)*>
<!-- variant constructor -->
<!ELEMENT vcon (gtype)*>
<!-- id: variant constructor name -->
<!ATTLIST vcon
id CDATA #REQUIRED>
<!-- TYPES -->
<!-- type: ground or function type -->
<!ELEMENT type (gtype | funtype)>
<!-- groundtype -->
<!ELEMENT gtype (tapply | tvar | top | state)>
B.4 Report DTD report.dtd
59
<!-- type application -->
<!ELEMENT tapply (gtype*)>
<!-- tcref: type constructor to be applied -->
<!ATTLIST tapply
tcref CDATA #REQUIRED>
<!-- type variable -->
<!ELEMENT tvar EMPTY>
<!-- id: type variable name -->
<!ATTLIST tvar
id CDATA #REQUIRED>
<!-- supertype of all other types -->
<!ELEMENT top EMPTY>
<!-- repository state -->
<!ELEMENT state EMPTY>
<!-- function type -->
<!ELEMENT funtype (type*,gtype)>
<!-- predicate type -->
<!ELEMENT predtype (type)*>
B.4
Report DTD report.dtd
<!-- CONSISTENCY REPORTS -->
<!-- rule evaluations (for each rule its report) -->
<!ELEMENT evaluations (evaluation*,repairs?)>
<!ELEMENT evaluation (rule,report)>
<!-- reports (description + S-DAG) -->
<!ELEMENT report (desc?,sdag)>
<!-- truth: report’s boolean truth value -->
<!ATTLIST report
truth (true | false) #REQUIRED><!-- report’s truth value -->
<!-- S-DAG -->
<!ELEMENT sdag (leaf | allofnq | oneofnq | allofq | oneofq | abandoned | ref)>
<!-- predicate leaf -->
<!ELEMENT leaf (desc?,suggestalternative*)>
<!-- psym: predicate symbol -->
<!-- cons: is psym responsible for an inconsistency? -->
<!-- result: boolean result of psym -->
60
DTDs
<!ATTLIST leaf
id CDATA #REQUIRED
psym CDATA #REQUIRED
cons (consistent | inconsistent) #REQUIRED
result (true | false) #REQUIRED>
<!-- alternative predicate suggestions set -->
<!ELEMENT suggestalternative (suggest*)>
<!-- predicate suggestion -->
<!ELEMENT suggest (sugsetsuchthat | sugdontknow | sugset | sugcontradict)>
<!-- set the value of a variable to the specified value -->
<!ELEMENT sugset (value)>
<!-- var: variable to set -->
<!-- field: field in the variable to set -->
<!-- cost: repair cost -->
<!ATTLIST sugset
var CDATA #REQUIRED
field CDATA #IMPLIED
cost CDATA #IMPLIED>
<!-- set a variable such that the specified predicate holds or not -->
<!ELEMENT sugsetsuchthat (value*)>
<!-- var: variable to set -->
<!-- bool: targeted boolean value -->
<!ATTLIST sugsetsuchthat
var CDATA #REQUIRED
bool (true | false) #REQUIRED>
<!-- don’t know how to change the variable -->
<!ELEMENT sugdontknow EMPTY>
<!-- var: variable to set -->
<!-- bool: targeted boolean value -->
<!ATTLIST sugdontknow
var CDATA #REQUIRED
bool (true | false) #REQUIRED>
<!-- contradicting suggestions, e.g. set x to 1 and keep x -->
<!ELEMENT sugcontradict (suggest*)>
<!-- S-DAG conjunction node -->
<!ELEMENT allofnq (sdag*)>
<!ATTLIST allofnq
id CDATA #REQUIRED>
<!-- S-DAG disjunction node -->
<!ELEMENT oneofnq (sdag*)>
<!ATTLIST oneofnq
id CDATA #REQUIRED>
B.4 Report DTD report.dtd
61
<!-- S-DAG universal node -->
<!ELEMENT allofq (domain?,quantedge*)>
<!-- id: quantified variable -->
<!ATTLIST allofq
var CDATA #REQUIRED
id CDATA #REQUIRED>
<!-- S-DAG existential node -->
<!ELEMENT oneofq (domain?,quantedge*)>
<!-- id: quantified variable -->
<!ATTLIST oneofq
var CDATA #REQUIRED
id CDATA #REQUIRED>
<!-- domain of a quantifier node -->
<!ELEMENT domain (value*)>
<!-- repair action -->
<!ELEMENT repairaction (delete | add | change | changesuchthat | keep)>
<!-- delete a value -->
<!ELEMENT delete (value)>
<!-- add a value -->
<!ELEMENT add (value)>
<!-- change a value (from, to) -->
<!ELEMENT change (value,value)>
<!-- field: change this field -->
<!ATTLIST change
field CDATA #IMPLIED>
<!-- change free variables of the corresponding formula such that -->
<!-- the predicate symbol applied to the given values results in ... -->
<!ELEMENT changesuchthat (value*)>
<!-- psym: predicate symbol which should be applied to the values -->
<!-- bool: requested boolean result -->
<!ATTLIST changesuchthat
psym CDATA #REQUIRED
bool (true | false) #REQUIRED>
<!-- do nothing -->
<!ELEMENT keep EMPTY>
<!-- edge below a quantifier node
(bound values, repair actions, target S-DAG) -->
<!ELEMENT quantedge (value*,repairaction*,sdag)>
62
DTDs
<!-- an abandoned S-DAG which we do not want to repair -->
<!ELEMENT abandoned EMPTY>
<!-- a reference to another S-DAG node -->
<!ELEMENT ref EMPTY>
<!ATTLIST ref
targetID CDATA #REQUIRED>
<!-- REPAIR collection -->
<!ELEMENT repairs (repairalt*)>
<!-- alternative repair set in the repair collection -->
<!ELEMENT repairalt (repair*)>
<!-- repair -->
<!ELEMENT repair (concerns*,term,assign*,repairaction,rating)>
<!-- rules for which a repair resolves inconsistencies -->
<!ELEMENT concerns EMPTY>
<!-- rule: rule identifier -->
<!-- var: variable inside the rule -->
<!ATTLIST concerns
rule CDATA #REQUIRED
var CDATA #REQUIRED>
<!-- repair context -->
<!ELEMENT assign (value)>
<!-- var: variable to which a value is assigned -->
<!ATTLIST assign
var CDATA #REQUIRED>
<!-- rating of a repair -->
<!ELEMENT rating (resolves*,offends*)>
<!-- cost: repair cost -->
<!ATTLIST rating
cost CDATA #IMPLIED>
<!-- how many inconsistencies does a rule resolve -->
<!ELEMENT resolves EMPTY>
<!-- ruleprio: priority of the rule for which inconsistencies are resolved -->
<!-- inconsistencies: number of inconsistencies resolved -->
<!ATTLIST resolves
ruleprio CDATA #REQUIRED
inconsistencies CDATA #REQUIRED>
<!-- rules that might be violated by apoplying a repair -->
<!-- rule: rule identifier of a possibly violated rule -->
<!ELEMENT offends EMPTY>
<!ATTLIST offends
B.4 Report DTD report.dtd
rule CDATA #REQUIRED>
<!-- VALUES -->
<!ELEMENT value (vat | vrec | vvar | vfun | vundefined)>
<!-- atomic value -->
<!ELEMENT vat (#PCDATA)>
<!-- record value -->
<!ELEMENT vrec (vlabel*)>
<!-- id: record constructor -->
<!ATTLIST vrec
id CDATA #REQUIRED>
<!-- record value label -->
<!ELEMENT vlabel (value)>
<!-- id: label name -->
<!ATTLIST vlabel
id CDATA #REQUIRED>
<!-- variant value -->
<!ELEMENT vvar (value*)>
<!-- id: variant constructor name -->
<!ATTLIST vvar
id CDATA #REQUIRED>
<!-- function value -->
<!ELEMENT vfun EMPTY>
<!-- id: name of the function -->
<!ATTLIST vfun
id CDATA #REQUIRED>
<!-- undefined value -->
<!ELEMENT vundefined EMPTY>
<!-- consistency rule -->
<!ELEMENT rule (meta,formula,actions)>
<!-- date: creation date of the rule -->
<!-if a rule is newer than the last runtime then
it might have been changed -->
<!-- id: rule identifier -->
<!ATTLIST rule
date CDATA #REQUIRED
id ID #REQUIRED> <!-- rule name -->
<!-- rule metadata -->
<!ELEMENT meta (desc?,precon*,docdeps?)>
63
64
DTDs
<!-- weight: rule weight (importance) 0 .. 100 -->
<!-- weak: may a rule be violated? -->
<!ATTLIST meta
weight CDATA "0"
weak (true | false) #REQUIRED>
<!-- consistency rule description -->
<!ELEMENT desc (#PCDATA)>
<!-- rule precondition: this rule must be satisfied in order to check -->
<!-- the current rule (not supported at the moment) -->
<!ELEMENT precon EMPTY>
<!ATTLIST precon
id CDATA #REQUIRED>
<!-- document dependencies of a rule -->
<!-- not given: dont know (determined by CDET) -->
<!-- given: these are the documents the rule really depends on -->
<!ELEMENT docdeps (docdep*)>
<!ELEMENT docdep EMPTY>
<!-- regex: regular expression of the dependent documents -->
<!ATTLIST docdep
regex CDATA #REQUIRED>
<!-- first order formula with description -->
<!ELEMENT formula
(desc?,(papply | or | and | not | implies | forall | exists))>
<!-- applied predicate (atomic formula) plus hint collection -->
<!ELEMENT papply (term*,hintalternative*)>
<!-- id: predicate symbol -->
<!ATTLIST papply
id CDATA #REQUIRED>
<!-- alternative hint set -->
<!ELEMENT hintalternative (set*)>
<!-- hint -->
<!ELEMENT set (term)>
<!-- condition: predicate result causing to execute the hint -->
<!-- id: variable to set -->
<!-- varcondition: set variable only if it is marked new / old -->
<!-- field: record field to set -->
<!-- repaircost: cost imposed by executing the corresponding repair -->
<!ATTLIST set
condition (true | false) #IMPLIED
id CDATA #REQUIRED
varcondition (new | old) #IMPLIED
B.4 Report DTD report.dtd
65
field CDATA #IMPLIED
repaircost CDATA #IMPLIED>
<!-- disjunction -->
<!ELEMENT or (formula,formula+)>
<!-- conjunction -->
<!ELEMENT and (formula,formula+)>
<!-- implication -->
<!ELEMENT implies (formula,formula)>
<!-- negation -->
<!ELEMENT not (formula)>
<!-- universal quantification with sphere term -->
<!ELEMENT forall (term,formula)>
<!-- id: quantified variable -->
<!-- action: hint for quantifier -->
<!-- keepdomain: also cache the quantifier sphere (may be expensive!) -->
<!ATTLIST forall
id CDATA #REQUIRED
action (delete | add | change | keep) #IMPLIED
keepdomain (true | false) #IMPLIED>
<!-- existential quantification with sphere term -->
<!ELEMENT exists (term,formula)>
<!-- id: quantified variable -->
<!-- action: hint for quantifier -->
<!-- keepdomain: also cache the quantifier sphere (may be expensive!) -->
<!ATTLIST exists
id CDATA #REQUIRED
action (delete | add | change | keep) #IMPLIED
keepdomain (true | false) #IMPLIED> <!-- quantified variable -->
<!-- TERMS -->
<!-- term with description -->
<!ELEMENT term (desc?,(var | fapply | sym | rec | case | typed))>
<!-- variable -->
<!ELEMENT var EMPTY>
<!-- id: variable name -->
<!ATTLIST var
id CDATA #REQUIRED>
<!-- applied function symbol -->
<!ELEMENT fapply (term*)>
<!-- id: function symbol name -->
66
DTDs
<!ATTLIST fapply
id CDATA #REQUIRED>
<!-- function symbol e.g. as argument for higher order functions -->
<!ELEMENT sym EMPTY>
<!-- id: function symbol name -->
<!ATTLIST sym
id CDATA #REQUIRED>
<!-- record construction -->
<!ELEMENT rec (label)*>
<!-- id: record constructor name -->
<!ATTLIST rec
id CDATA #REQUIRED>
<!-- record label -->
<!ELEMENT label (term)>
<!-- id: label name (unique for this record) -->
<!ATTLIST label
id CDATA #REQUIRED>
<!-- variant deconstruction -->
<!ELEMENT case (term,binding*)>
<!-- tcref: variant constructor (type constructor) -->
<!ATTLIST case
tcref CDATA #IMPLIED>
<!-- binding inside case: id -> sym -->
<!ELEMENT binding EMPTY>
<!-- id: variant constructor -->
<!-- sym: function symbol to be applied to constructor arguments -->
<!ATTLIST binding
id CDATA #REQUIRED
sym CDATA #REQUIRED>
<!-- explicitly typed term -->
<!ELEMENT typed (term,type)>
<!-- user defined action what should be done with the report -->
<!-- not supported at the moment -->
<!ELEMENT actions (mailreport*, mailrepair*,mailsummary?)>
<!-- Mail the report to some recipients -->
<!-- not supported at the moment -->
<!ELEMENT mailreport (recipient+)>
<!ATTLIST mailreport
currentonly (true | false) #REQUIRED
B.4 Report DTD report.dtd
explain
format
attachDocs
(true | false) #REQUIRED
(xml | latex) #REQUIRED
(true | false) #REQUIRED>
<!-- Mail the repair suggestions to some recipients -->
<!-- not supported at the moment -->
<!ELEMENT mailrepair (recipient+)>
<!ATTLIST mailrepair
currentonly (true | false) #REQUIRED
explain
(true | false) #REQUIRED
format
(xml | latex) #REQUIRED
attachDocs (true | false) #REQUIRED>
<!-- Mail a comprehensive summary to some recipients -->
<!-- not supported at the moment -->
<!ELEMENT mailsummary (recipient+)>
<!ELEMENT recipient EMPTY>
<!ATTLIST recipient
mailto CDATA #REQUIRED>
<!-- TYPES -->
<!-- type: ground or function type -->
<!ELEMENT type (gtype | funtype)>
<!-- groundtype -->
<!ELEMENT gtype (tapply | tvar | top | state)>
<!-- type application -->
<!ELEMENT tapply (gtype*)>
<!-- tcref: type constructor to be applied -->
<!ATTLIST tapply
tcref CDATA #REQUIRED>
<!-- type variable -->
<!ELEMENT tvar EMPTY>
<!-- id: type variable name -->
<!ATTLIST tvar
id CDATA #REQUIRED>
<!-- supertype of all other types -->
<!ELEMENT top EMPTY>
<!-- repository state -->
<!ELEMENT state EMPTY>
<!-- function type -->
<!ELEMENT funtype (type*,gtype)>
67
Appendix C
GNU General Public License
Version 2, June 1991
c 1989, 1991 Free Software Foundation, Inc.
Copyright 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA
Everyone is permitted to copy and distribute verbatim copies of this license
document, but changing it is not allowed.
Preamble
The licenses for most software are designed to take away your freedom to share and change
it. By contrast, the GNU General Public License is intended to guarantee your freedom
to share and change free software—to make sure the software is free for all its users.
This General Public License applies to most of the Free Software Foundation’s software
and to any other program whose authors commit to using it. (Some other Free Software
Foundation software is covered by the GNU Library General Public License instead.) You
can apply it to your programs, too.
When we speak of free software, we are referring to freedom, not price. Our General
Public Licenses are designed to make sure that you have the freedom to distribute copies
of free software (and charge for this service if you wish), that you receive source code or
can get it if you want it, that you can change the software or use pieces of it in new free
programs; and that you know you can do these things.
To protect your rights, we need to make restrictions that forbid anyone to deny you
these rights or to ask you to surrender the rights. These restrictions translate to certain
responsibilities for you if you distribute copies of the software, or if you modify it.
For example, if you distribute copies of such a program, whether gratis or for a fee,
you must give the recipients all the rights that you have. You must make sure that they,
too, receive or can get the source code. And you must show them these terms so they
know their rights.
We protect your rights with two steps: (1) copyright the software, and (2) offer you this
license which gives you legal permission to copy, distribute and/or modify the software.
Also, for each author’s protection and ours, we want to make certain that everyone
understands that there is no warranty for this free software. If the software is modified
by someone else and passed on, we want its recipients to know that what they have is
not the original, so that any problems introduced by others will not reflect on the original
authors’ reputations.
Finally, any free program is threatened constantly by software patents. We wish to
avoid the danger that redistributors of a free program will individually obtain patent
68
69
licenses, in effect making the program proprietary. To prevent this, we have made it clear
that any patent must be licensed for everyone’s free use or not licensed at all.
The precise terms and conditions for copying, distribution and modification follow.
GNU GENERAL PUBLIC LICENSE
TERMS AND CONDITIONS FOR COPYING,
DISTRIBUTION AND MODIFICATION
0. This License applies to any program or other work which contains a notice placed
by the copyright holder saying it may be distributed under the terms of this General
Public License. The “Program”, below, refers to any such program or work, and
a “work based on the Program” means either the Program or any derivative work
under copyright law: that is to say, a work containing the Program or a portion of
it, either verbatim or with modifications and/or translated into another language.
(Hereinafter, translation is included without limitation in the term “modification”.)
Each licensee is addressed as “you”.
Activities other than copying, distribution and modification are not covered by this
License; they are outside its scope. The act of running the Program is not restricted,
and the output from the Program is covered only if its contents constitute a work
based on the Program (independent of having been made by running the Program).
Whether that is true depends on what the Program does.
1. You may copy and distribute verbatim copies of the Program’s source code as
you receive it, in any medium, provided that you conspicuously and appropriately
publish on each copy an appropriate copyright notice and disclaimer of warranty;
keep intact all the notices that refer to this License and to the absence of any
warranty; and give any other recipients of the Program a copy of this License along
with the Program.
You may charge a fee for the physical act of transferring a copy, and you may at
your option offer warranty protection in exchange for a fee.
2. You may modify your copy or copies of the Program or any portion of it, thus
forming a work based on the Program, and copy and distribute such modifications
or work under the terms of Section 1 above, provided that you also meet all of these
conditions:
(a) You must cause the modified files to carry prominent notices stating that you
changed the files and the date of any change.
(b) You must cause any work that you distribute or publish, that in whole or
in part contains or is derived from the Program or any part thereof, to be
licensed as a whole at no charge to all third parties under the terms of this
License.
(c) If the modified program normally reads commands interactively when run,
you must cause it, when started running for such interactive use in the most
ordinary way, to print or display an announcement including an appropriate
copyright notice and a notice that there is no warranty (or else, saying that
you provide a warranty) and that users may redistribute the program under
these conditions, and telling the user how to view a copy of this License.
(Exception: if the Program itself is interactive but does not normally print
such an announcement, your work based on the Program is not required to
print an announcement.)
70
GNU General Public License
These requirements apply to the modified work as a whole. If identifiable sections
of that work are not derived from the Program, and can be reasonably considered
independent and separate works in themselves, then this License, and its terms, do
not apply to those sections when you distribute them as separate works. But when
you distribute the same sections as part of a whole which is a work based on the
Program, the distribution of the whole must be on the terms of this License, whose
permissions for other licensees extend to the entire whole, and thus to each and
every part regardless of who wrote it.
Thus, it is not the intent of this section to claim rights or contest your rights to
work written entirely by you; rather, the intent is to exercise the right to control
the distribution of derivative or collective works based on the Program.
In addition, mere aggregation of another work not based on the Program with
the Program (or with a work based on the Program) on a volume of a storage or
distribution medium does not bring the other work under the scope of this License.
3. You may copy and distribute the Program (or a work based on it, under Section
2) in object code or executable form under the terms of Sections 1 and 2 above
provided that you also do one of the following:
(a) Accompany it with the complete corresponding machine-readable source code,
which must be distributed under the terms of Sections 1 and 2 above on a
medium customarily used for software interchange; or,
(b) Accompany it with a written offer, valid for at least three years, to give any
third party, for a charge no more than your cost of physically performing
source distribution, a complete machine-readable copy of the corresponding
source code, to be distributed under the terms of Sections 1 and 2 above on a
medium customarily used for software interchange; or,
(c) Accompany it with the information you received as to the offer to distribute
corresponding source code. (This alternative is allowed only for noncommercial distribution and only if you received the program in object code or
executable form with such an offer, in accord with Subsection b above.)
The source code for a work means the preferred form of the work for making modifications to it. For an executable work, complete source code means all the source
code for all modules it contains, plus any associated interface definition files, plus
the scripts used to control compilation and installation of the executable. However,
as a special exception, the source code distributed need not include anything that is
normally distributed (in either source or binary form) with the major components
(compiler, kernel, and so on) of the operating system on which the executable runs,
unless that component itself accompanies the executable.
If distribution of executable or object code is made by offering access to copy from
a designated place, then offering equivalent access to copy the source code from the
same place counts as distribution of the source code, even though third parties are
not compelled to copy the source along with the object code.
4. You may not copy, modify, sublicense, or distribute the Program except as expressly
provided under this License. Any attempt otherwise to copy, modify, sublicense or
distribute the Program is void, and will automatically terminate your rights under
this License. However, parties who have received copies, or rights, from you under
this License will not have their licenses terminated so long as such parties remain
in full compliance.
5. You are not required to accept this License, since you have not signed it. However, nothing else grants you permission to modify or distribute the Program or
71
its derivative works. These actions are prohibited by law if you do not accept this
License. Therefore, by modifying or distributing the Program (or any work based
on the Program), you indicate your acceptance of this License to do so, and all its
terms and conditions for copying, distributing or modifying the Program or works
based on it.
6. Each time you redistribute the Program (or any work based on the Program),
the recipient automatically receives a license from the original licensor to copy,
distribute or modify the Program subject to these terms and conditions. You may
not impose any further restrictions on the recipients’ exercise of the rights granted
herein. You are not responsible for enforcing compliance by third parties to this
License.
7. If, as a consequence of a court judgment or allegation of patent infringement or
for any other reason (not limited to patent issues), conditions are imposed on you
(whether by court order, agreement or otherwise) that contradict the conditions
of this License, they do not excuse you from the conditions of this License. If you
cannot distribute so as to satisfy simultaneously your obligations under this License
and any other pertinent obligations, then as a consequence you may not distribute
the Program at all. For example, if a patent license would not permit royalty-free
redistribution of the Program by all those who receive copies directly or indirectly
through you, then the only way you could satisfy both it and this License would be
to refrain entirely from distribution of the Program.
If any portion of this section is held invalid or unenforceable under any particular
circumstance, the balance of the section is intended to apply and the section as a
whole is intended to apply in other circumstances.
It is not the purpose of this section to induce you to infringe any patents or other
property right claims or to contest validity of any such claims; this section has the
sole purpose of protecting the integrity of the free software distribution system,
which is implemented by public license practices. Many people have made generous
contributions to the wide range of software distributed through that system in
reliance on consistent application of that system; it is up to the author/donor to
decide if he or she is willing to distribute software through any other system and a
licensee cannot impose that choice.
This section is intended to make thoroughly clear what is believed to be a consequence of the rest of this License.
8. If the distribution and/or use of the Program is restricted in certain countries
either by patents or by copyrighted interfaces, the original copyright holder who
places the Program under this License may add an explicit geographical distribution
limitation excluding those countries, so that distribution is permitted only in or
among countries not thus excluded. In such case, this License incorporates the
limitation as if written in the body of this License.
9. The Free Software Foundation may publish revised and/or new versions of the
General Public License from time to time. Such new versions will be similar in
spirit to the present version, but may differ in detail to address new problems or
concerns.
Each version is given a distinguishing version number. If the Program specifies a
version number of this License which applies to it and “any later version”, you have
the option of following the terms and conditions either of that version or of any
later version published by the Free Software Foundation. If the Program does not
specify a version number of this License, you may choose any version ever published
by the Free Software Foundation.
72
GNU General Public License
10. If you wish to incorporate parts of the Program into other free programs whose
distribution conditions are different, write to the author to ask for permission. For
software which is copyrighted by the Free Software Foundation, write to the Free
Software Foundation; we sometimes make exceptions for this. Our decision will be
guided by the two goals of preserving the free status of all derivatives of our free
software and of promoting the sharing and reuse of software generally.
NO WARRANTY
11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS
NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING
THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES PROVIDE THE
PROGRAM “AS IS” WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE PROGRAM
PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO
IN WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY
WHO MAY MODIFY AND/OR REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED
INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR
A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED
OF THE POSSIBILITY OF SUCH DAMAGES.
END OF TERMS AND CONDITIONS
Bibliography
[AHV96]
S. Abiteboul, L. Herr, and J. Van den Bussche. Temporal versus firstorder logic to query temporal databases. In ACM Symp. on Principles
of Database Systems, pages 49–57, Montreal, Canada, 1996. ACM
Press.
[C+ 03]
M. Chakravarty et al. The Haskell Foreign Function Interface 1.0
(Addendum to the Haskell 98 Report), 2003.
see www.cse.unsw.edu.au/˜chak/haskell/ffi/.
[CSFP04]
B. Collins-Sussman, B. W. Fitzpatrick, and C. M. Pilato. Version
Control with Subversion. O’Reilly and Associates, 2004.
[MTH90]
R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML.
MIT Press, 1990.
[PJ03]
S. L. Peyton-Jones. Haskell 98 Language and Libraries: The Revised
Report. Cambridge University Press, 2003.
[Rou05]
D. Roundy. DARCS: David’s advanced revision control system, 2005.
see www.darcs.net.
[SBBS05]
J. Scheffczyk, U. M. Borghoff, A. Birk, and J. Siedersleben. Pragmatic
consistency management in industrial requirements specifications. In
Proc. of the 3rd IEEE Int. Conf. on Software Engineering and Formal
Methods, page to appear, Koblenz, Germany, 2005. IEEE CS Press.
[SBRS03a] J. Scheffczyk, U. M. Borghoff, P. R¨odig, and L. Schmitz. Consistent
document engineering. In Proc. of the 2003 ACM Symp. on Document
Engineering, pages 140–149, Grenoble, France, 2003. ACM Press.
[SBRS03b] J. Scheffczyk, U. M. Borghoff, P. R¨odig, and L. Schmitz. Efficient (in) consistency management for heterogeneous repositories. In Proc. of
the 4th Int. Conf. on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing, pages 370–377, L¨
ubeck,
Germany, 2003. ACIS.
[SBRS04a] J. Scheffczyk, U. M. Borghoff, P. R¨odig, and L. Schmitz. Managing
inconsistent repositories via prioritized repair actions. In Proc. of the
2004 ACM Symp. on Document Engineering, pages 137–146, Milwaukee, WI, 2004. ACM Press.
73
74
BIBLIOGRAPHY
[SBRS04b] J. Scheffczyk, U. M. Borghoff, P. R¨odig, and L. Schmitz. Towards efficient consistency management for informal applications. Int. Journal
of Computer & Information Science, 5(2):109–121, 2004.
[SBRS04c] J. Scheffczyk, Uwe M. Borghoff, P. R¨odig, and L. Schmitz. S-DAGs:
Towards efficient document repair generation. In Proc. of the 2nd
Int. Conf. on Computing, Communications and Control Technologies,
volume 2, pages 308–313, Austin, TX, 2004. University of Texas at
Austin.
[Sch04]
J. Scheffczyk. Consistent Document Engineering. PhD thesis, Universit¨at der Bundeswehr M¨
unchen, 2004. see www.unibw.de/inf2/CDET.
[SSBS04]
J. Scheffczyk, C. Stutz, U. M. Borghoff, and J. Siedersleben. Formale
Konsistenzsicherung in informellen Software-Spezifikationen. Informatik Forschung und Entwicklung, 19(1):17–29, 2004.
[W3C01]
World Wide Web Consortium W3C. XML Schema part 0: Primer.
W3C Recommendation, 2001. see www.w3.org/TR/xmlschema-0/.
[WR99]
M. Wallace and C. Runciman. Haskell and XML: Generic combinators
or type-based translation? In Proc. of the 4th ACM SIGPLAN Int.
Conf. on Functional Programming, pages 148–159, Paris, France, 1999.
ACM Press.