Foundations of Software Engineering

Tetsuo Tamai
Chapter 8

Formal Methods

All of the models introduced in the previous chapters were described using diagrams. While the meaning of diagrams is
intuitively easy to understand, they inevitably lack logical rigor.
In this chapter, we discuss how to impart rigor to model descriptions by using a formal description format similar to
that used in mathematics and logic.

8.1 Meaning of Formal Methods

One method of modeling is abstraction through formalization, as used in mathematics and logic. Form literally means
”shape,” regardless of content. Natsume Soseki had a firm understanding of formal logic in this sense. The following
passage appears in the tenth chapter of ”I Am a Cat.”
”I believe that the relationship between these two is like the nouns in a proposition of formal logic, connected
regardless of their content.”
Formal logic, also known as mathematical logic or symbolic logic, is a symbolic formalization of logic since Aristotle.
It formally defines the grammar and inference rules that make up logical expressions using symbols, and as Soseki said,
there is arbitrariness in how these symbols are linked to the real world. The ”form” in formal methods for software
development has roughly the same meaning as the form of formal logic.
The significance of using formal methods in software development is as follows:
1. Applying formal methods to specification descriptions to create rigorous, unambiguous specifications.
2. Verifying the correctness of the written specifications and models and the properties they possess.
3. Verifying that implemented programs satisfy their specifications.
4. Systematically or automatically synthesize programs from formal specifications.
If these goals could be achieved, formal methods would become a powerful tool in software engineering, and they
have long been studied. However, despite their long history, their adoption in industry has yet to reach a sufficient stage.
Formal methods have long been used to design logic circuits and communication protocols, where their effectiveness is
quite clear. However, the application of formal methods to general software is not as easy due to the much larger state
space, and their adoption has been limited. Relatively advanced applications are in fields requiring high reliability, such
as space equipment, aircraft, and nuclear reactor control. However, much modern software requires high security and
confidentiality. Therefore, following the success of fields such as aerospace and nuclear reactor control, the scope of
application has expanded. Furthermore, the moderate cost of using formal methods can be justified for widely and repeat-
edly used products such as middleware, libraries, components, and services that is, products that are highly reusable and
standardized.
There is also a valid criticism that ”human thinking is not formal.” However, because formal methods are also invented
by humans, it can be said that humans are capable of thinking both formally and informally. This ability to switch flexibly
is one of the great advantages of the human brain. When people read formal descriptions, they do not necessarily pursue
formal reasoning, and even if they do go to the trouble of following it, that alone does not make them feel like they
”understand.” People understand formal descriptions by relating them to some kind of model in their own mind.
Even if people do not normally think formally, they sometimes formalize things because it saves thought. Even in
such cases, value is created in the ability to move freely between formal and informal methods. However, when faced
with a real-world problem and a formalization that fits the bill is discovered, not only does it often make it easier to arrive
at the solution, but the beauty of the form itself can also be moving.
Below, we will look at the diverse techniques used in formal methods, aiming for each of their goals.

1
8.2 Formal Specification
Efforts to expand the scope of formal specification techniques to include practical system development are particularly
active in Europe. From the perspective of industrial application, emphasis is placed on rigorous specification description,
while proving the correctness of the developed software or automatic program generation is not necessarily the primary
focus. [16]
The reason for this active activity in Europe is, of course, due in part to the strong tradition of mathematics and logic,
but the influence of the Esprit project, which was promoted by the then EC (now the EU) in the 1980s, is also likely to
be significant. In the 1980s, Japan undertook a national project to develop a ”fifth-generation computer” over a 10-year
period. The project is commonly referred to as the ICOT project, named after the organization that led it, the Institute
for Future Computer Technology (ICOT). Inspired by this, Esprit, which was born in Europe, broadened its scope to
include LSI development technology and software engineering. Furthermore, the development framework not only spans
the EC’s various countries, but also aims to foster collaboration between industry and academia. As a result, attempts to
apply formal methods, such as Z, originally developed in universities, to industry have been promoted. Several formal
specification languages have been proposed, but as we will see below, they are not just specification languages; software
development methodologies using them have also been proposed and implemented.

8.2.1 VDM
Although the name VDM[21] is rarely mentioned anymore, it originally descended from the Vienna Definition Language,
which provides the operational semantics of programming languages. Today, it has completely moved away from the
framework of operational semantics and, instead, while influenced by denotational semantics, has come to refer to a
specification description notation based on predicate logic expressions and the program development techniques based
on it. There are two schools of thought: a British one centered around Cliff Jones and a Danish one centered around
Dines Bjørner, and the notations used in these two schools differ somewhat. Support tools for the VDM-SL specification
language based on VDM have also been developed and licensed, and there are known examples of its use in practical
system development. [13]

8.2.2 Z
Z[27] is a formal specification language based on set theory, developed primarily at Oxford University in the UK. It
was influenced by VDM and shares many similarities, but its notation has been refined to be more concise. Examples
of practical applications often cited include the use of this language to describe the entire specification for IBM’s CICS
data communication management system, thereby improving maintainability and achieving groundbreaking results in
reducing errors in new versions. [25, 17] Also, the use of a formal specification for floating-point arithmetic to develop
actual arithmetic elements. [3] The former is known for its large scale, involving a 2,000-page specification written in Z
and the development of a program of approximately 50,000 lines based on it. Furthermore, by comparing the use of Z
with the use of Z, data showed a several-fold improvement in reliability and a 9

8.2.3 RAISE
RAISE (Rigorous Approach to Industrial Software Engineering)[8] was developed as part of the European Esprit project,
led by Bjørner, who led VDM in Europe, and also emphasizes mathematical formalism. It defined RSL as a specification
language and developed a software development methodology using it. RSL differs from VDM and other methods in that
it not only allows for declarative descriptions, but also includes basic elements for imperative descriptions and concurrent
behavior descriptions.
Bjorner, a professor at the Technical University of Denmark, was involved in the establishment of the United Nations
University International Institute for Software Technology (UNU-IIST) in Macau in 1992 and served as its first director.
He then applied formal methods using RAISE to the development of railway computer systems in mainland China. [4]
After returning to Denmark, he published a three-volume series of books on software engineering, centered around RSL
programming. [6, 7, 5]

8.2.4 B and Event-B

Jean-Raymond Abrial, who had a major influence on the development of Z, also created a formal specification language
called B. [1] Furthermore, Event-B explicitly adds a representation for describing events to B[2]. Development method-
ologies based on B and Event-B are characterized by thorough proof-reading at each step of gradual refinement from the
very beginning, and this method has been applied to the development of the Paris subway system and an automated bus
system.

2
8.2.5 Algebraic Specification Languages
Algebraic specification languages are another lineage. Representative examples include the OBJ family of languages
started by Joseph Goguen. Among them, CafeOBJ, developed by Kokichi Niki and others in Japan, has a highly refined
language and processing system[12]. At the same time, in Europe, Donald Sannella, Andrzej Tarlecki and others designed
a specification language called Casl (the Common Algebraic Specification Language) and created a processing system
for it[26], and at SRI in the United States, Jose Meseguer and others created an algebraic specification language called
Maude and an excellent processing system for it[22].

8.2.6 Lotos and Estell

Languages used to describe the specifications of parallel systems, particularly communication protocols, include Lotos
and Estell. Systems that generate programs from these specifications have also been developed. Because the specification
and development of parallel systems is generally prone to errors, formal development techniques are likely to be effective.
Formal methods were introduced relatively early on to the specification of standard protocols and languages.

8.2.7 Alloy
Alloy is a language for describing software models invented by Daniel Jackson. Its foundation is relational logic, and like
Z, it is based on set theory. However, its notation has been improved to make it lightweight, and an analysis tool called
the Alloy Analyzer has been developed and is in practical use. Inspired by model checking systems (described below),
the Alloy Analyzer can automatically verify various properties of a model by limiting its scope to small, finite sets. [20]
Daniel Jackson is the son of Michael Jackson.

8.2.8 Property-Oriented vs. Model-Oriented

The methods used for such formalization can be classified as property-oriented or model-oriented. Property-oriented
methods use an axiomatic approach to define the external properties of the system being specified, while model-oriented
methods constructively define the internal structure that forms those properties. A representative example of property-
oriented methods is a semantic definition method like CafeOBJ, which uses algebraic specifications. A representative
example of model-oriented methods is a method like Z or VDM, which defines the specifications of a state machine using
the data structures that make up its state and the input/output specifications for its operations.
For example, when specifying a stack, an algebraic specification would express the basic properties using axioms
expressed as equations, such as ”push and pop” returning to the original state. However, in Z or VDM, it is common to
define it constructively using sequences, for example.

8.3 Verifying Correctness

As introduced in Chapter ??, E. W. Dijkstra said, ”Testing can show that a program has bugs, but it cannot show that it
does not.” In that sense, testing cannot verify that a program is completely correct. If ”completeness” is desired, the only
way to mathematically prove that the target program satisfies its specifications is to combine formal specifications with
the program’s formal semantics. Such research has been ongoing since the 1970s and has been applied to some programs
that require particularly high reliability. While there are not yet many examples of its application to general programs,
this technique has had a significant impact on programming language design and programming methodology.

8.3.1 Method of Correctness Proof

The steps for formally proving the correctness of a program are roughly as follows:
1. Correctness Proof
• Describe the specifications in terms of pre- and post-conditions.
• Place an invariant assertion for loops. You may insert any other assertions.
• For a program execution path that has preconditions, postconditions, and assertions before and after it, prove
that the final condition can be derived from the first condition of the path.
In this case, Hoare-style axioms are used to explain the meaning of each program element. (Alternatively,
language elements can be interpreted as ”transforming” the program state expressed by predicates.)

3
 2. Termination Proof
In addition to proving that the result is correct, it is necessary to guarantee that the program terminates correctly.
Correctness that includes termination is called strong correctness. This is usually demonstrated by showing that
some value (e.g., a nonnegative integer) with a finite descending chain order, i.e., an order with the property that a
monotonically decreasing sequence is necessarily finite, monotonically decreases with each iteration of the loop.

The concept of pre- and post-conditions and invariants is also adopted in ”design by contract,” an object-oriented
development methodology proposed by Bertrand Meyer. [23] When designing an object’s methods, the pre- and post-
conditions are first described, which are then treated as a contract. The design is then carried out to abide by that contract.
Conditions that always hold for a class are described as invariants, which also become the class design contract. Users
look at the contract and trust that the object will behave in accordance with it.
By describing pre-conditions as assertions that can be checked at runtime, you can verify whether the assertions hold
true at runtime, without using tools like a theorem prover. If they do not, you can issue a warning or interrupt the program.
However, there is a restriction: general logical expressions cannot be written as pre- and post-conditions or invariant
assertions; only those that are determined as logical values at runtime are valid.
To support contract-based design, UML also introduced OCL (Object Constraint Language)[29] as a language for
describing preconditions, postconditions, and invariants, and its use in combination with class diagrams is recommended.
Once formal specifications can be created, it should be possible to mathematically verify whether a program developed
in accordance with those specifications satisfies them. Various verification methods have been devised for this purpose,
with the primary early achievement being Floyd-Hoare logic.

8.3.2 Floyd-Hoare Logic

Floyd-Hoare logic was independently proposed by Tony Hoare and Robert W. Floyd around the same time. Due to the
similarities in their concepts, it later came to be called Floyd-Hoare logic.[18, 14].
Floyd presented a logical verification method for flowcharts, while Hoare focused on Pascal programs. Therefore,
Hoare’s paper, published in CACM in 1969, is monumental not only for presenting a method for program verification, but
also for proposing an axiomatic semantics for programming languages (in this case, a sublanguage of Pascal).
Program code and preconditions/postconditions in Hoare logic are written as follows:
{P}C{Q}
Here, C is a piece of program code, P is a logical condition that must be true before C is executed, and Q is a logical
condition that must be true after C is executed and terminated. In imperative languages, the semantics of assignment
statements, which assign values to program variables, require particular attention. Hoare wrote it as follows:
{P[f/x]} x:=f {P}
Here, P is an arbitrary logical formula, and the precondition {P[f/x]} represents a formula in which all occurrences of
the variable x in P are replaced with the value f.
The next issue is how to handle loop (repetition) structures. Therefore, we introduce the concept of loop invariants. A
loop invariant is a condition that must always hold when execution enters a loop. Therefore, the loop rule can be written
as follows:
If {P ∧ B}S{P} then {P} while B do S {¬B ∧ P}
By appropriately specifying such a loop invariant and further specifying preconditions and postconditions as specifica-
tions for the entire program, and repeatedly applying the axioms and inference rules defined for each program statement,
the program code will eventually disappear, leaving only the logical formulas. If this can be proven, the target program
will have been verified to satisfy its specifications.

8.3.3 Theorem Provers

Proving correctness manually cannot guarantee that the proof is error-free. For this reason, various theorem provers have
been created and tested. Theorem provers cannot be fully automated. Therefore, a human must take the time to develop
a proof strategy and introduce necessary lemmas. Another problem is that if a proof fails, it is not immediately clear
whether the problem is with the program, the specifications, the proof strategy, or the capabilities of the proof system.
However, theorem provers have long been developed in the field of artificial intelligence, not just for program veri-
fication. Their capabilities have steadily improved throughout their history. Below, we provide an overview of the main
theorem provers that are particularly relevant to program verification.

8.3.4 LCF
LCF (Logic for Computerable Functions) is a theorem prover developed by Robin Milner in the early 1970s. [15]. It is
an interactive theorem prover. The programming language ML (Meta Language), developed at that time to allow users to

4
describe their theorem-proving strategies, is still used today as a common functional programming language, along with
its derivatives such as OCaml.

8.3.5 Isabelle/HOL
Isabelle/HOL is a theorem prover that has been under development since the 1980s, succeeding LCF. [24] It is released
as free software and has been widely used, resulting in a rich library of accumulated proofs.

8.3.6 Coq
Like Isabelle/HOL, Coq is an interactive theorem prover that has been under development since the 1980s. Like Is-
abelle/HOL, it is positioned as a proof assistant. Its development was led by a group including Thierry Coquand and
Gérard Huet at INRIA in France. Its development language was primarily OCaml, which also ties it to the lineage of LCF.

8.3.7 ACL2
Robert Boyer and Strother Moore, then at the University of Texas at Irvine, developed a unique theorem prover using Lisp
in the 1970s. This later evolved into a new system called Nqthm, and is now available as open source software called
ACL2. It is characterized by its automated proof system for inductive logic and is primarily used for verifying software
and hardware. It is developed in Common Lisp.

8.3.8 PVS
PVS (Prototype Verification System) is a theorem proving system developed primarily by John Rushby of SRI in the
United States, specifically for verifying computer programs. It is developed in Common Lisp and is available under the
GPL (GNU License).

8.4 Model Checking

Model checking, while a formal method, has significant differences compared to the verification techniques using theorem
proving discussed in the previous section.
Simply put, model checking is a method for automatically verifying whether a model expressing a system’s specifi-
cations satisfies the system’s required properties. In particular, for reactive systems that include concurrency, the model
is described using a Labeled Transition System (LTS) and the properties are expressed using temporal logic. This term is
often used in a narrower sense to refer to systems where the model is described using a Labeled Transition System (LTS)
and the properties are expressed using temporal logic. [11] Here, a Labeled Transition System can be considered essen-
tially the same as the state machine introduced in Section ??, except that the events attached to each transition that cause
the transition are called labels. Furthermore, since this technique is intended to model reactive systems, the existence of
final states is not assumed. A structure in which a subset of atomic propositions is labeled on vertices rather than edges is
also commonly used in model checking techniques; this is called a Kripke structure.
Model checking, a methodology first proposed in the early 1980s, was used to verify the correctness of hardware logic
circuits and communication protocols, but has since come to be used to verify general software models as well. Compared
to theorem-proving verification, it has the following differences:
1. The target of verification is a program model, not the program itself. However, various methods have been devised
for applying model checking to programs in combination with techniques for automatically generating models from
programs, such as Java Pathfinder[28].
2. The specifications to be verified are generally not the complete program specification, but rather an extracted portion
of the specification’s properties related to safety and liveness.

3. While theorem proving systems generally require human intervention in the proof process, such as providing lem-
mas, model checking systems, when properly configured, can perform the work automatically and produce results.
4. If verification fails, counterexamples that do not satisfy the specification are output, providing reference for error
correction.

5
8.4.1 Temporal Logic
Temporal logic, which describes the properties to be verified, adds time-related modal operators, such as ”always” and
”someday,” to general propositional logic. There are various types of temporal logic, but the most commonly used are
linear temporal logic (LTL) and computation tree logic (CTL).
LTL was first proposed by Amir Pnueli in 1977, marking the beginning of the development of temporal logic for
computer science. Meanwhile, CTL was proposed by Edmund Clarke and Allen Emerson at Carnegie Mellon University
(CMU) in the early 1980s, and software for automated model checking was developed based on it. This is the basis for the
current model checking system, NuSMV. [10] The forerunner of LTL-based model checking systems is SPIN, developed
by Gerard J. Holzmann and his group at Bell Labs. Development of SPIN also began in the early 1980s, but it wasn’t until
1991 that it became available to the public for free [19].
LTL and CTL were devised independently, and their processing systems were developed separately. However, Emer-
son et al. later proposed CTL* as a temporal logic system that encompasses both, clarifying the relationship between LTL
and CTL. This relationship is shown in Figure 8.1.

Figure 8.1: CTL, LTL and CTL*

LTL and CTL do not subsume one another. There are expressions that can be expressed in LTL but not in CTL, and
conversely, there are expressions that can be expressed in CTL but not in LTL. However, CTL* subsume both LTL and
CTL, and there are expressions that can be expressed in CTL* but not in either LTL or CTL.
CTL* uses the following five temporal operators:
1. X p: Means ”next.” Indicates that p will be true in the next state.
2. F p: Means ”someday.” Indicates that p will be true someday during future state transitions.
3. G p: Means ”always.” Indicates that p will always be true during future state transitions.

4. p U q: Means ”until.” Indicates that p will remain true until q is true during future state transitions.
5. p R q: Means release. Indicates that q will remain true until p is first true during future state transitions. q is released
only when p is true, but it is not required that p will necessarily be true at some point.
Apart from these, there are two other types of path quantifiers related to branching computations:

1. E f: There is a path from the current state in which f is true.

2. A f: f holds for all transition paths from the current state.
Note that the operators ¬, ∨, and∧ used in standard propositional logic are also used. These logical operators are not
all independent; five operators are sufficient: ∨, ¬, X, U, and E. The others can be expressed using combinations of these.
CTL adds the following constraint to CTL* : ”When the temporal operators X, F, G, U, and R appear, they must be
immediately preceded by the path quantifier E or A.” LTL is a CTL* with the added restriction that ”items of the form A
f are allowed, where f does not include a path quantifier.”

8.4.2 Properties to be Checked

Properties that are the subject of model checking are typically divided into two types.

6
 • SafetyThe property that an undesirable event never occurs, regardless of the transition path taken. A typical example
of an undesirable event is a deadlock. Resource access violations (such as mutual exclusion violations) are also
typical undesirable events in concurrent systems. Temporal logic formulas are usually written in the following
pattern:

AG ¬P

• LivenessThe property that a desirable event will always occur. What is desirable depends on the system’s functional
requirements, but a typical example is a property in a client/server system where a service request from a client is
always provided at some point. In temporal logic, this is usually described in the following pattern:

AF Q

To understand safety and liveness more concretely, let’s consider what properties can be expected from the examples
of the sake warehouse problem and the vending machine problem we’ve used so far.
First, regarding safety, the vending machine problem description itself shows some consideration for safety.

• When the purchase button for a product whose sales lamp is lit is pressed, the lamp flashes and one item is dispensed
into the dispenser. At the same time, the balance is deducted by the product’s price. No money can be inserted
during this time.
• When the refund button is pressed, the remaining balance at that time is refunded to the change dispenser. Money
cannot be inserted during the refund process.

The bolded portion above requests that money insertion be blocked during processing when the purchase button or
refund button is pressed. This is likely a consideration of inconsistencies in the management of the inserted amount due to
simultaneous decrease and increase operations. While the problem description reads as a requirement to physically block
money insertion, it is possible to implement mutual exclusion of amount data in software so that money insertion does not
appear blocked to the user. Furthermore, if a specific blocking is implemented, care must be taken to avoid deadlock and
proper testing is required.
As for liveness, consider the sake warehouse problem, where the requirement that customer orders be shipped at some
point is an example of liveness. To fulfill this requirement, merely designing the system is insufficient; it is necessary to
assume an external business condition that ensures that enough sake to satisfy an order will always be available at some
point. Accurately describing this condition and designing the logic accordingly is surprisingly difficult. For example,
suppose we assume a condition that when an order is made that results in an out-of-stock item, there will always be a
cumulative delivery of the ordered item that exceeds the shortage. However, if shipping is a first-in, first-out strategy,
meaning that earlier orders are shipped first, can we guarantee that the order will always be shipped at some point? If you
think about it, there are cases where this does not work. Even if there is a cumulative delivery that exceeds the shortage,
if a single delivery is always below the shortage, then the order will be overtaken by a later order of the same item in a
smaller quantity. If this situation continues all the time, the customer will be kept waiting forever. It would seem that it
would be good to set the condition that there will always be a single delivery that exceeds the shortage, but then it could
be argued that this condition is too strict.

8.4.3 Kripke Structure

A Kripke structure associates a set of atomic propositions as labels with each state of a state machine. While states, which
are the vertices of a graph, are labeled, transitions, which are the edges of the graph, are not. Formally, a Kripke structure
is represented by the following quadruple:

(S, S0 , R, L)

S is a set of states, S0 is a subset of S and represents the initial state. R is a subset of S × S and represents the transition
relation. This relation is a global relation, i.e., for any state s ∈ S, there must exist s′ ∈ S such that R(s, s′ ) holds.
If AP is a set of atomic propositions, then the label L is a function from S to the power set of AP (a set whose elements
are subsets of AP), i.e., L : S → 2AP .
Let’s look at an example. Figure 8.2 shows a Kripke structure diagram for a simplified example of a drink vending
machine.
Here, the AP consists of the following five atomic propositions:
{receive coins, purchasable, sold, change, juice}
The meaning of each is as follows:

7
 Figure 8.2: Kripke structure of a vending machine

• receive coins: coins have been received.

• purchaseable: drinks can be purchased.
• sold: drinks have been sold.
• change: change can be returned.

• juice: juice is selected as an available drink. In the negative case, cola is selected.
Let’s assume the property to be verified is the following CTL formula:
AG (receive coins → AF sold)
As you can see from the diagram, whether this holds can be determined by searching paths on the Kripke structure.
In fact, model checking mechanizes and verifies such path search. As is clear from this example, it is possible to loop
infinitely between vertices 1 and 2 on the Kripke structure, i.e., inserting coins and receiving change can be repeated
forever. Therefore, the above formula does not hold unless appropriate fairness assumptions are made. However, if we
rewrite the property as follows, it holds true.
AG (receive coins → AFchange ∨ sold)

8.4.4 Representing Boolean Expressions

As can be seen from the Kripke structure example, model checking requires the evaluation of logical expressions at each
state. The efficiency of this process determines the overall performance of model checking. The basis is the evaluation
of a propositional logical expression based on the truth value of each element of a set of atomic propositions, which, as
has long been known, boils down to the evaluation of a Boolean function. A Boolean function can be viewed as a feature
function defining a set of variable vectors for which it is true. Therefore, a set can be represented by defining a method
for expressing a Boolean expression.

8
8.4.5 Binary Decision Diagrams
CMV, developed at CMU in the 1980s, introduced a data structure called a binary decision diagram (BDD), which suc-
cessfully reduced data volume and accelerated decision procedures. A Boolean function of n variables can be computed
simply by creating an n-level binary tree. However, this results in a lot of structural duplication, resulting in waste in terms
of both storage space and computational complexity. Binary decision diagrams (BDDs) are a clever way to eliminate this
duplication. However, the size of a BDD varies depending on the order of the variables, and determining the optimal order
is computationally intractable, so heuristic methods are used. However, a BDD that specifies a single variable order and
fixes it regardless of the path from the root to the leaves of the tree yields a canonical system, so ordered binary decision
diagrams (OBDDs) are often used. Our group at CMU called this method using OBDDs ”symbolic model checking,”
since it performs model checking without expressing specific states.

8.4.6 Bounded Model Checking and SAT

The introduction of BDDs has dramatically improved execution speed, but it still often fails to address state explosion,
particularly due to system concurrency. However, model checking is useful if it can uncover cases that do not satisfy
required properties, and based on the experience that when a model has a flaw, the computational path leading to the flaw
is often relatively short in practice, a method was proposed and put into practical use: limiting the length of the path to be
searched to within an appropriate constant k. This method is called bounded model checking.
Since a set of states can be represented using Boolean functions as feature functions, the transitions from state to
state can also be represented as Boolean functions. By restricting the number of transitions to a finite value k or less,
determining whether a target Kripke structure satisfies a given temporal logic formula reduces to the Boolean function
satisfiability problem (SAT). The satisfiability problem has been tackled in the field of artificial intelligence since the early
days of theorem proving, and has long been known to be NP-complete. The Davis–Putnam algorithm, published in 1960,
is famous; while it does not break the NP-completeness barrier, it is known as a practical method. Subsequently, SAT
solvers based on this algorithm and incorporating various improvements have been developed and put into use. Bounded
model checking techniques have also become more effective by utilizing existing SAT solvers.
Furthermore, ”satisfiability modulo theory” (SMT) has been proposed, which extends the satisfiability problem to
allow predicates in logical formulas and combines specialized theories with these predicates. Various SMT solvers have
been developed, including Microsoft’s Z3 Theorem Prover.

8.4.7 Abstraction
Another effective approach to addressing state explosion is state space abstraction. Two methods are known: one considers
a state space limited to only variables that affect the specification, and the other abstracts the data space. We will discuss
the latter here.
For example, if even one of the elements constituting a state takes an integer value, the number of possible values
becomes infinite. An example of abstraction is mapping this to three levels, for example, 0, positive, negative.
This abstraction reduces the state space, and if the property to be checked can be expressed in that abstract space, model
checking can be performed. Generally, properties that hold in an abstract space also hold in the original space. However,
properties that do not hold in the abstract space may hold in the original space. Therefore, even if a counterexample is
detected in an abstracted problem, it is necessary to further refine the abstraction and evaluate whether it is a meaningful
counterexample. Such counterexamples in abstract spaces are called spurious counterexamples, and there have been
various research studies on how to deal with them. [9].

8.5 Application Example—Describing the Sake Store Warehouse Problem in

Z
As an application example of formal methods, we will consider describing the ”Sake Store Warehouse Problem” using
the specification language Z.
As introduced in Section 8.2.2, Z is a formal specification language developed at Oxford University. It is based on set
theory, and all data is typed based on set theory. Schemas are a framework for describing the information units composed
of such data sets, their properties, and the operations that can be performed on them. They play a central role in the Z
language.

8.5.1 Types in Z
All objects (expressions) expressed in Z have types. A type can be considered a set, but it can either be a predefined basic
set or a structure constructed from such sets. A typical basic set is the set of integers (written as Z in Z), but many are

9
defined for individual problem domains.
In our problem, we take ”container number” and ”item name” as given basic data sets. We also use the name ”quantity”
as a natural number (greater than or equal to 1) that does not include zero. This is written as follows:

[containernumber, itemname]
Quantity == N1

In general,

[identifier, . . . , identifier]

introduces the name of the basic type (set). In the following description of Z, we will use the types introduced here as
given without delving into their internal structure.
Also,

variablen ame == expression

we can refer to the expression on the right-hand side by the name on the left-hand side.
Structural types constructed from basic types include power set types, Cartesian product types, and schema types,
examples of which will appear in subsequent sections.

8.5.2 schema
Now, a warehouse is filled with containers. Let’s represent this as a schema named ”warehouse.”

warehouse
Container : containern umber →
7 (itemn ame →
7 quantity)

A schema generally consists of a schema name, a declaration section, and an axiom section. The entire structure is
enclosed in a rectangular box with an open right side. The schema name is written within the horizontal line at the top
of the box. The declaration and axiom sections are written within a rectangle, separated by a horizontal line. However,
this example only consists of the declaration section, with no axiom section. This declaration section shows a single
variable, ”container,” representing the state of the warehouse, along with its type. In general, the declaration section
of a schema can contain multiple variable declarations. This allows such a schema to be considered a record-type data
declaration. However, since variable types generally include functions, it is closer to the object concept in object-oriented
programming.
The type of this container is indeed a function. The symbol → 7 represents a partial function, so the container can be read
as a partial function with the container number as its domain and (productname → 7 quantity) as its range. Furthermore,
the range (productname → 7 quantity) is itself a partial function, with the product name as its domain and the quantity as
its range. In other words, the container is a collection of product names with a defined quantity.
The Z approach also interprets such functions in a set-theoretic sense. In other words, the type of a set of containers
is:

Container ∈ P(ContainerNumber × P(ItemName × Quantity))

Here, P is the operation that creates a power set. That is, P X is the set of subsets of X. Also, X × Y is the operation
that creates the Cartesian product of X and Y. That is, the elements of X × Y are the ordered pair (x, y) of element x of X
and element y of Y.
Z is characterized by its ability to view functions and relationships as sets. Functions from domain X to Y and
relationships between domains X and Y are both viewed as subsets of the Cartesian product X × Y, and their basic types
are assumed to be the same. A function is a type of relation, subject to the constraint that for any element of the domain,
there is at most one pair containing that element.
The type of relation between sets X and Y is written as X ↔ Y. In Z, this is defined as

X ↔ Y == P(X × Y)

This means that a relation R has the type X ↔ Y, i.e., R : X ↔ Y means that R ∈ P(X × Y), meaning that R as a set has
the form {(x1 , y1 ), (x2 , y2 ), . . . , (xm , ym )}, where xi ∈ X, yi ∈ Y(i = 1, . . . , m).
For a relation X ↔ Y, there are standardly defined functions called dom and ran, of type (X ↔ Y) → P X and
(X ↔ Y) → P Y, respectively. For a relation R, dom R represents its domain, and ran R represents its range.

10
 Treating relations and functions as sets in Z is not particularly difficult, but it is easy to confuse types with values or
the type hierarchy. For example, if we consider a type R such that R == P P S, then a variable declaration x : R of type R,
or a predicate x ∈ R that says x is an element of R, will result in the value of x being one of the subsets of S. Furthermore,
if we define y ∈ x, then the value of y is one of the subsets of S. Furthermore, if we define z ∈ y, then the value of z is an
element of S.
In this way, the left-hand side of a type declaration or predicate ∈ is one level lower than the right-hand side in the
hierarchy of set-of-set relations. On the other hand, raising the hierarchical level of a set not only occurs when P is applied
directly, but also when using relations and functions, as can be seen from the definition of relations, so be careful when
you’re not familiar with it.
The axiom section of a schema specifies the constraints that the variables defined in the declaration section must satisfy.
In this example, if the constraint given in the problem statement is ”Up to 10 brands can be mixed in one container,” the
schema can be written as follows:

warehouse
Container : Containernumber →
7 (productname →
7 quantity)
∀ c : dom container • #(container c) ≤ 10

Here, as already mentioned, dom is a function that takes a function (generally a relation) as an argument and specifies its
domain, and # is a function that takes a finite set as an argument and specifies the number of elements in that set. Both
are defined as standard functions in Z.
The axiom section contains predicate logical formulas. The following logical operators are used:
¬ negation
∧ conjunction
∨ disjunction
⇒ implication
∀ universal
∃ existence
Universal binding logical formulas are generally written as follows:

∀ declaration[; declaration; . . .] • logicalformula

Here, declaration is:

declaration ::= variablename[, variablename, . . .] : type
where type is an expression representing a set. The same applies to existential binding logical formulas.
Note that multiple logical formulas may be written side by side in the axiom section of a schema, separated by line
breaks. In this case, the whole is considered to consist of the conjunction of the logical expressions on each line. In other
words, a line break can be used instead of a conjunction symbol.
In Z, predicates are also interpreted set-theoretically. That is, when the predicate P(x) is written, P represents a set,
and its meaning is equivalent to x ∈ P. Therefore, new predicates are also defined by constructively giving sets.

8.5.3 General Definitions

Higher-Order Functions The problem is the process of shipping in response to customer orders. Customers order a
certain number of bottles of sake with a certain name. To fulfill this order, it is necessary to search the warehouse for
containers of sake by name. To do this, let’s consider the concept of sake inventory.

Sakeinventory : Name →
7 (Containernumber →
7 Quantity)

Add this to the warehouse declaration. The type of sake inventory can be expressed as a set type:

sakeinventory ∈ P(productname × P(containernumber × quantity))

The key to this problem is that the container and the sake inventory are essentially the same thing.
To do this, let’s generalize a bit. The types of containers and sake inventory have the form (X →7 (Y →7 Z)), which can
be converted one-to-one to ((X × Y) → 7 Z). This conversion is the exact opposite of the currying operation in functional
programming, which turns a multivariate function into a sequence of single-variable functions. So, let’s define a bijective
(higher-order) function uncurry that converts functions of type (X → 7 (Y → 7 Z)) to functions of type ((X × Y) → 7 Z).
When defining this function, the target types X, Y, Z do not need to be specific; they can generally be any type. Z provides
a convenient notation format for defining generic functions using types as parameters, called a generic definition. It is
written as follows:

11
 [X, Y, Z]
uncurry : (X →
7 (Y →
7 Z)) ↣
→ ((X × Y) →
7 Z)
∀ f : (X → 7 (Y →7 Z)) •
uncurry f =
{ x : X; y : Y; z : Z | x ∈ dom f ∧ y ∈ (f x) ∧ z = f x y • (x, y) 7→ z }

This defines a global function uncurry with arbitrary types, X, Y, and Z, as parameters. The axioms below the middle
line define the properties of the function. Here, ↣
→ represents a bijection. 1 Also, x 7→ y represents a pair that maps value
x to value y as an element of a function. That is, if x 7→ y ∈ f , then f (x) = y. Corresponding to the set representation,
x 7→ y is actually the same as (x, y). Note that in Z, following the conventions of functional programming, parentheses
are generally not used unless needed to express function application. Therefore, f (x) is usually written as f x.
This function definition uses set comprehension notation, which generally takes the following form:

{D | P • E}

Here, D is a variable declaration, P is a logical expression representing a constraint, and E is an expression. D represents
the set of values obtained by selecting only those values within the range of the type of the variable declared in D that
satisfy the logical expression P and substituting them for E. For example, {x : N1 | x ≤ 5 • x2 } is equivalent to
{1, 4, 9, 16, 25}. Universal and existential binding logical expressions also use • as a delimiter, but care must be taken, as
appropriate parentheses may be required to avoid confusion with set comprehension notation.
Note that E can be omitted, in which case it represents the set of D values that satisfy P. For example, {x : N1 | x ≤ 5}
is equivalent to {1, 2, 3, 4, 5}. In practice, this form may be more commonly used.
Now that we’ve seen how to write predicate logical expressions and set comprehension notation, let’s look at defining
functions using both. As mentioned earlier, a function is a type of relation such that for any element of the domain, there
is at most one pair containing it. This is defined in Z as follows:

X→
7 Y == {f : X ↔ Y | (∀ x : X; y1 , y2 : Y •
(x 7→ y1 ) ∈ f ∧ (x 7→ y2 ) ∈ f ⇒ y1 = y2 )}

(Note that the • in this expression is not the • used in set comprehension notation, but the • of a universal binding.)
Now that we’ve used uncurry to convert a container into a function of two arguments, we’ll consider a conversion that
swaps the first and second arguments.

[X, Y, Z]
swap : ((X × Y) →
7 Z) ↣
→ ((Y × X) →
7 Z)
∀ f : (X × Y) →
7 Z•
swap f = { x : X; y : Y; z : Z | (x, y) ∈ dom f ∧ z = f (x, y) • (y, x) 7→ z }

Finally, this series of transformations can be expressed as uncurry∼ ◦ swap ◦ uncurry. Here, ◦ represents the composi-
tion of functions, and uncurry∼ represents the inverse function of uncurry (injective functions can have inverse functions).
It is natural to name this inverse function curry, so we will set it as follows.

curry == uncurry∼

Using these, we can rewrite the warehouse schema as follows:

warehouse
Container : Containernumber →7 (productname →7 quantity)
Alcoholinventory : Productname →
7 (containernumber →
7 quantity)
Alcoholinventory = curry ◦ swap ◦ uncurry container

multiset When a shipping request is received, we need to determine whether there is enough alcohol of the specified
brand in stock to fulfill the order. Also, if a container is empty, there is a request to remove the container, so we may need
the total amount of alcohol currently in the container. The function that gives these values would be:

Brandinventory : Productname → 7 quantity

Containerinventory : Containernumber → 7 quantity
1 Bijection means both surjection and injection. f : X →
7 Y is surjective if its range covers the entire Y, i.e., if ran f = Y. It is also called a mapping
from X onto Y. An injective is a one-to-one mapping, and f : X → 7 Y is injective if ∀ x1 , x2 : dom f • f x1 = f x2 ⇒ x1 = x2 .

12
Let’s write out the specifications for these two functions.
Comparing these functions with the definitions of sake inventory and container, the relationship between them be-
comes clear. Like sake inventory, brand inventory has the domain of product name, and is the sum of the quantities
mapped to it containernumber → 7 quantity. Similarly, container inventory can be considered the sum of the quantities for
the elements in the container range. This can be formally described.
For example, for productname → 7 quantity, or equivalently, for the elements of P(productname × quantity), we first
consider the operation of collecting the quantities, which are the second components of each, and then take the sum. To
do this, it seems appropriate to use the function ran, which is generally defined for relations. However, the problem is
that it is inconvenient to consider the collection of second components as a set. While a set does not consider duplicate
elements, in this case, even if the same quantity of values appears multiple times, they must be treated as separate entities.
Such a collection is called a multiset (also called a bag or multiset).
In Z, a multiset consisting of elements a1 , . . . , an is written as [[a1 , . . . , an ]]. For example, [[1, 2, 2, 3]] is different from
[[1, 2, 3]] (however, since the order is irrelevant, [[1, 2, 2, 3]] is the same as, for example, [[1, 2, 3, 2]]). Z defines a multiset
as a function from the elements to natural numbers greater than or equal to 1. The natural number to which it is mapped
represents the number of occurrences in the multiset. That is, in general, a multiset bag X of type X is defined as

bag X == X →
7 N1

For example, [[1, 2, 2, 3]] is an element of bag N, which, by definition, is represented as {1 7→ 1, 2 7→ 2, 3 7→ 1}.
We want a multiset version of dom and ran, which are defined in Z for relations. Let’s call them bdom and bran, and
define them as follows:

[X, Y]
bdom : (X ↔ Y) → bag X
bran : (X ↔ Y) → bag Y
∀R : X ↔ Y •
bdom R = { x : dom R • x 7→ #{ y : Y | x R y} } ∧
bran R = { y : ran R • y 7→ #{ x : X | x R y} }

Next, let’s define a function Σ that sums the elements of a multiset of natural numbers Z.

Σ : bag Z → Z
Σ[[]] = 0
∀ x : Z • Σ[[x]] = x
∀ B, C : bag Z • Σ(B ] C) = ΣB + ΣC

The notation used here, which lacks the outer framework of a schema, is called an axiomatic statement. It declares global
variables and provides their properties as axioms. Variables declared in a schema cannot be referenced without referenc-
ing the schema name, but variables declared in an axiomatic statement are global and can be referenced at any time. In
this respect, they are similar to variables declared in a generic definition. However, the difference is that a generic defi-
nition defines parameterized global variables (usually functions), while an axiomatic statement defines constant variables
(functions).
Note that [[]] represents the empty multiset, and the symbol ] represents the operation of taking the union of two
multisets.
Functions like Σ can also be generalized and defined for multisets bag X over sets X that have identity elements and
commutative and associative binary operations.
However, here we do not go that far and instead define it for addition over the natural numbers.
Based on the above, let us define the transformation to obtain brand inventory and container inventory from sake
inventory and container inventory, respectively, as a (higher-order) function called subtotal:

[X, Y]
subtotal : (X →
7 (Y →
7 Z)) → (X → Z)
∀f : X →
7 (Y →
7 Z) • subtotal f = { x : dom f • x 7→ Σ ◦ bran ◦ f x }

Using this, we obtain:

Brandinventory == subtotal sakeinventory

Containerinventory == subtotal container

13
 Let’s expand and redefine the warehouse schema to include these two functions.

warehouse
Container : Containernumber → 7 (productname → 7 quantity)
Alcoholinventory : Productname → 7 (containernumber →
7 quantity)
Brandinventory : Productname → 7 quantity
Containerinventory : Containernumber → 7 quantity
Alcoholinventory = curry ◦ swap ◦ uncurry container
Brandinventory == subtotal alcoholinventory
Containerinventory == subtotal container

8.5.4 Abstract Machine

Up until now, descriptions using Z have primarily captured the static aspects of the problem domain in question. This
approach has been to use abstract functions to capture the logical structure of the target as concisely as possible. However,
one of Z’s key features is its ability to treat targets as stateful abstract machines and describe their dynamic behavior.
Schemas are often used for this purpose.

Operation Specification For example, a warehouse schema has so far been treated as a specification of the space of
possible values for a data type with components such as containers and sake inventory. When considering this as an
abstract machine, we imagine a machine (or process, or system) whose state at any given time is one of these values.
The machine’s state changes depending on external operations. To represent this state change, we need a mechanism for
describing the relationship between the state before and after the operation.
For example, let’s consider the process of receiving containers into storage.

StockEntry
Warehouse
Warehouse′
cn? : Containernumber; s? : Productname →
7 Quantity
cn? 6∈ dom Container
Container′ = Container ∪ {cn? 7→ s?}

This schema definition uses an important notation: quoting and qualifying other schemas. First, the ”Warehouse”
schema is quoted. In this case, the declaration part of the quoted schema is directly added to the declaration part of the
”StockEntry” schema defined here, and its axioms are directly added to the axiom part of ”StockEntry”. On the other
hand, the notation ”warehouse′ ” is a qualified schema reference. It means that all variables declared in the warehouse
declaration (container, sake inventory, container inventory, brand inventory) are prefixed with ”′ ”, and all of those variables
appearing in the axioms section are also replaced with ”′ ”. These ”′ ” variables are usually interpreted as indicating the
state of the schema representing the ”stocking” operation we are defining here, after the operation is completed.
Since it is common for schemas defining state machine operations to cite both the schema representing the state and
the schema with ”′ ” prefix, a notation has been established to express both at the same time. This is done by prefixing the
schema name to be referenced with ∆ (the capital Greek letter delta). That is, in the above example,

Stocking
∆Warehouse
cn? : Containernumber; s? : Productname →
7 Quantity
cn? 6∈ dom Container
Container′ = Container ∪ {cn? 7→ s?}

Input/Output Conditions This schema also introduces two variables, cn? and s?. Variables with a suffix of ? are
interpreted as representing input data for this operation. Also, although not shown in this example, variables represent-
ing output are typically followed by an ! However, these are merely a convenient convention for interpreting them as
representing state machine operations; in logical expressions, they are simply variables just like ordinary variables.
The axioms of such an operation’s schema represent the input and output conditions of the operation. Many formal
specification languages other than Z (e.g., VDM) syntactically distinguish between input and output conditions, but Z
does not make such a distinction. However, among the logical formulas that make up the axioms (which are interpreted

14
as a conjunction of the whole), those that do not contain any variables suffixed with ”′ ” or ”!” can be interpreted as input
conditions, and those that contain even one can be interpreted as output conditions. Therefore, Z has adopted a policy of
not introducing syntactic elements that distinguish between input and output conditions.
This ”′ ” notation is powerful, especially since it automatically incorporates the axioms of cited schemas, eliminating
the need to explicitly write conditions that are invariant across operations. In the above example, the output condition
for ”container” is described, but not for ”sake inventory.” This is because the reference to the qualified schema implicitly
establishes the following (added to the axioms section of the inventory schema):

sakei nventory′ = curry ◦ swap ◦ uncurry container′

This approach is unique to Z and convenient, but it can sometimes make the operation specification difficult to understand.

Reference-Type Operations Some operations may refer to the state without changing it. In such cases, prefixing the
quoted schema with Ξ (Greek capital letter xi) not only simultaneously references that schema and the schema with ”′ ,”
but also implicitly adds the equation x = x′ to the axioms section for all variables x declared in the schema, just as if you
prefixed it with ∆.
For example, let’s define a reference operation that specifies a product and checks its stock quantity using the already
defined function ”product inventory quantity.”

Checkproductinventoryquantity
ΞWarehouse
b? : Productname, v! : Quantity
v! = Productinventoryquantity b?

Initialization For a state machine, its initial state must be determined somehow. This can also be defined as a schema.
For the warehouse, for example,

InitialWarehouse
Warehouse
Container = ∅

If we defined this as an initialization operation, we would use ∆ warehouse and set Container′ = ∅. However, the
above definition is a declarative description of the warehouse’s initial state.

Error Handling The ”warehouse” operation requires that the container number of the container being stored does not
match the container number of a container already in the warehouse (cn? 6∈ dom Container). How should we describe the
exceptions that occur when this condition is not met? In Z, the standard practice is to describe such exception handling
specifications separately as a separate schema.
First, we define an ”error condition,” a type consisting of symbols for identifying errors.

ErrorCondition ::= normal | duplicatecontainernumber

Here, ::= is a free-form declarator that declares a type consisting of elements listed on the right-hand side, separated by
|. In this example, it is a simple enumeration type, but recursive definitions are possible, allowing for the introduction of
recursively defined types, such as tree types.
Next, we define a schema representing the normal case as ”normal completion.”

Successful
Result! : Errorcondition
Result! = Normal

This may seem like a trivial schema, but it becomes useful by using a mechanism called schema expressions. A schema
expression connects schemas with operations. There are several types of operators, but here we will only discuss the
logical schema operators ∧ and ∨. Both take two schemas and construct a new schema. In both cases, the declaration
parts of the two schemas are merged. If a variable with the same name exists in both schemas, the intersection of the types
(sets) of those variables in each schema is taken, and a single variable of that type is declared in the resulting schema.
Furthermore, the axiom part is the conjunction of the axiom parts of the two schemas in the case of ∧, and the disjunction
of the axiom parts of the two schemas in the case of ∨.

15
 Therefore, if we define ”warehouse entry ∧ successfully completed,” the previously defined warehouse entry will have
the added functionality of returning a successful result.
Next, the case where a duplicate container number occurs can be described using the following schema.

DuplicateNumber
ΞWarehouse
cn? : ContainerNumber
Result! : ErrorCondition
cn? ∈ dom Container
Result! = DuplicateContainerNumber

Using this, the warehouse entry operation, including exception conditions, can be written as follows:

b (warehouseentry ∧ successfullycompleted) ∨ DuplicateNumber

GeneralizedWarehouseEntry =

Here, =b defines the schema on the left side using the schema expression on the right side.
After this, we need to deal with the ”shipping process” to complete the specification, but since this is somewhat
tedious and the essential parts of the specification have already been completed, we will leave it in a separate accessible
location. Furthermore, as a different type of application example using EventB, we will also include an application
example on the subject of ”bridge signal control.” Interested readers should refer to the ”Formal Methods Application
Example Supplement” [30]

16
Bibliography

[1] J.-R. Abrial. The B-book: assigning programs to meanings. Cambridge University Press, 2005.

[2] J.-R. Abrial. Modeling in Event-B: system and software engineering. Cambridge University Press, 2010.
[3] G. Barrett. Formal Methods Applied to a Floating-Point Number System. IEEE Trans. Softw. Eng., 15(5):611–621,
1989.
[4] D. Bjørner. Formal software techniques for railway systems. IFAC Proceedings Volumes, 33(9):101–108, 2000.

[5] D. Bjørner. Software Engineering 3: Domains, requirements, and software design. Springer Science & Business
Media, 2006.
[6] D. Bjørner. Software Engineering 1: Abstraction and modelling. Springer Science & Business Media, 2007.
[7] D. Bjørner. Software Engineering 2: Specification of systems and languages. Springer Science & Business Media,
2007.
[8] S. Brock and C. George. RAISE Method Manual (RAISE/CRI/DOC/3/V1). Computer Resources International, 1990.
[9] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In International
Conference on Computer Aided Verification, pages 154–169. Springer, 2000.

[10] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal
logic. In Workshop on Logic of Programs, pages 52–71. Springer, 1981.
[11] E. M. J. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
[12] R. Diaconescu and K. Futatsugi. CafeOBJ Report — The Langauage, Proof Techniques, and Methodologies for
Object-Oriented Algebraic Specification. World Scientific, 1998.

[13] J. Fitzgerald and P. G. Larsen. Modelling Systems. Cambridge University Press, 1998. :
2003
[14] R. W. Floyd. Assigning meanings to programs. In Program Verification, pages 65–81. Springer, 1993.
[15] M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF: a mechanised logic of computation, volume 78
of LNCS. 1979.
[16] A. Hall. Seven myths of formal methods. IEEE Software, pages 11–18, September 1990.
[17] I. Hayes. Specification Case Studies, 2nd ed. Prentice-Hall, 1992.
[18] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580,
1969.
[19] G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):1–17, 1997.
[20] D. Jackson. Software Abstractions: logic, language, and analysis. MIT press, 2012.
[21] C. B. Jones. Systematic Software Development using VDM, 2nd ed. Prentice Hall, 1990.

[22] J. Meseguer. Twenty years of rewriting logic. The Journal of Logic and Algebraic Programming, 81(7-8):721–781,
2012.
[23] B. Meyer. Object-Oriented Software Construction 2nd Edition. Prentice Hall International, 2000.

17
[24] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283.
Springer Science & Business Media, 2002.
[25] M. Phillips. CICS/ESA 3.1 experiences. In J. E. Nicholls, editor, Z User Workshop: Proceedings of the Fourth
Annual Z User Meeting, Oxford 1989. Springer-Verlag, 1990.
[26] D. Sannella and A. Tarlecki. Foundations of algebraic specification and formal software development. Springer
Science & Business Media, 2012.
[27] J. M. Spivey. The Z Notation — A Reference Manual, Second Edition. Prentice Hall, 1992.
[28] W. Visser, C. S. Pǎsǎreanu, and S. Khurshid. Test input generation with Java PathFinder. In Proceedings of the 2004
ACM SIGSOFT international symposium on Software testing and analysis, pages 97–107, 2004.

[29] J. Warmer and A. Kleppe. The Object Constraint Language : Precise Modeling with UML. Addison-Wesley, 1998.
[30] . . [Link]
[Link], 2021.

18