S-Program Calculus
ALEKSANDAR KUPUSINAC and DUŠAN MALBAŠKI1

arXiv:1003.0773v1 [cs.LO] 3 Mar 2010

Abstract
This paper presents a special subset of the first-order predicate logic named S-program
calculus (briefly S-calculus). The S-calculus is a calculus consisting of so-called S-formulas
that are defined over the abstract state space of a virtual machine. We show that S-formulas
are a highly general tool for analyzing program semantics inasmuch as Hoare triplets of total
and partial correctness are not more than two S-formulas. Moreover, all the rules of Hoare
logic can be derived using S-formulas and axioms/theorems of first-order predicate calculus.
The S-calculus is a powerful mechanism for proving program correctness as well as for building additional proving tools using theorems of the predicate logic. Every proof is based on
deriving the validity of some S-formula, so the procedure may be automated using automatic
theorem provers (we will use Coq in this paper). As an example of the use of S-calculus, we
will prove the four basic properties of Dijsktra’s operator wp. The proofs given by Dijkstra
are not completely formalized and we will show that a full formalization can be achieved using
S-calculus. Finally, we add one more theorem to the above-mentioned four, namely the law
of negation.
Key words: first-order predicate logic, Hoare logic, formal methods, program correctness,
program semantics, weakest precondition

1

Introduction

The key motivation for this research is the idea that programs may be treated as predicates
and/or Boolean expressions [28][24][19][32][23][20][21]. The connection between Floyd-Hoare logic
[15][22] and predicate logic is outlined in the papers of Cook [10] and Blass and Gurevich [7],
where they use it to analyze the completeness of Hoare logic [2]. Blass and Gurevich consider
the possibility of incorporating first-order predicate logic into Hoare logic, but they conclude that
it would significantly increase the complexity of the latter. In our opinion, it is not necessarily
the case: it is possible to generalize the ideas of Hoare logic on the abstract state space and
simultaneously simplify proofs, if the interpretation domain is strictly separated from the domain
of the abstract state space. Back, Akademi and von Wright [3] have developed the idea of a
special program calculus called refinement calculus, which was meant to combine Hoare’s ideas
with predicate logic. They solved the problem of indeterminism in the total/partial correctness
formulas by introducing additional formulas of angelical and demonical correctness [4], but at the
price of increasing the complexity of refinement calculus. Our idea is to develop a program calculus
that associates Hoare logic with first-order predicate logic and clearly separates the interpretation
domain from the abstract state domain (similarly to [27]). Secondly, it must not have any problems
with indeterminism. Finally, it must treat total/partial correctness directly, i.e. without any
requirement for additional concepts and formulas.
In this paper, we will present the development of S-program calculus (briefly S-calculus), which
represents a mathematical tool for the program semantics analysis [26]. Generality of the S-calculus
stems from the fact that it is built around so-called S-formulas that are defined on the abstract
state space and not on any of its interpretations, which was the reason for naming it ”S-calculus”,
after the word ”state”. Simultaneously with the development of S-calculus, we will discuss the
following six issues:
1 Authors’

address: A. Kupusinac and D. Malbaški, University of Novi Sad, Faculty of Technical Sciences, Trg
Dositeja Obradovića 6, 21000 Novi Sad, Serbia. {sasak, malbaski}@uns.ac.rs

2

A. Kupusinac and D. Malbaški

1.) The S-calculus uses an abstract state space and is a general tool for describing program
semantics.
2.) Hoare’s formulas of total and partial correctness are no more than two particular S-formulas.
3.) The S-calculus is based on the axioms and theorems of first-order predicate logic. The
assignment statement and standard syntax units (such as if-then, if-then-else, while etc.) are
defined using S-formulas so there is no need for special axioms and rules, as in Hoare logic.
4.) Variable declaration is also described using appropriate S-formulas.
5.) The general rules of Hoare logic are theorems in S-calculus and can be derived using axioms
and theorems of first-order predicate logic.
6.) Proofs in the S-calculus are simple since they rely only on the results of first-order predicate
logic. Moreover, they lend themselves to automation using standard theorem provers, making
it easier to introduce new rules and theorems.
The axiomatic system of S-calculus consists of the axioms of first-order predicate calculus. Each
theorem in the predicate calculus is also a theorem in the S-calculus and vice versa. In Section 2,
we will present the basic components, the axioms and several theorems in the S-calculus.
Hoare logic incorporates the formulas of total and partial correctness, the assignment axiom
and numerous rules [1][17]. The formulas of total and partial correctness are customarily denoted
respectively by {P }S{Q} and P {S}Q and their meaning is given in a descriptive form. Instead
of this, the S-calculus introduces strict mathematical notation for both formulas treating them as
two special S-formulas. This will be discussed in Section 2.
In Section 3, we will show that the general rules of Hoare logic are theorems in the S-calculus
that can be derived using solely the axioms and theorems of predicate logic. It follows that Hoare
logic is a special case of the S-calculus and consequently a special case of first-order predicate logic.
Hoare’s assignment axiom and the rules for special syntax units are not needed in the S-calculus.
They are considered as special S-formulas or, more precisely, as S-relations, where the term ”Srelation” refers to a binary relation on the abstract state space. For example, the assignment
statement a := e; is an interpretation of the appropriate S-relation Sa:=e; introduced by definition.
In Section 4, we will show the definitions of S-relations, the interpretations of which are the
statements no-operation, assignment, if-then-else, if-then, while and the sequence. In addition,
we will introduce a special S-formula whose interpretation is variable declaration. Owing to its
generality, the S-calculus allows variable definition to be considered as a special syntax unit, which
is a problem in theories that use interpreted state space [8][12][16][17][30]. This opportunity is
especially important for programming languages in which the declaration is an ordinary statement
(as in Java), because it makes automated correctness proofs possible [27].
Dijkstra has formulated the four basic theorems concerning the weakest precondition wp: the
law of the excluded miracle, the law of monotonicity, the law of conjunction and the law of disjunction. From the mathematical point of view, these proofs are not strictly formal [14][18]. In
Section 5, we will prove these theorems in a strictly formal way. In addition, we will prove the
fifth basic law, namely the law of negation. Finally, we will provide the formal proof of Dijkstra’s
theorem on total correctness.
The aim of this paper is not to lessen the importance of Hoare logic. On the contrary, we try to
generalize the basic ideas by raising its domain to the level of abstract state space. The S-calculus
is supposed to serve as a mathematical bridge between Hoare logic and the formalism of classical
predicate calculus. Connecting Hoare’s ideas with predicate logic is of significant importance. In
such connection Hoare logic is an appropriate mechanism for describing program syntax, while in
its background predicate logic stays with its powerful mathematical proving tools. Accordingly,
proving program correctness [13][5], as well as building new theorems in the S-calculus conforms
to the validity proofs of appropriate S-formulas. Based on that, we may conclude that for proving

S-Program Calculus

3

program correctness and new theorems we need rather uncomplicated mathematical tools such as
axioms, theorems and proving procedures of first-order predicate logic [9][11][25][29]. Moreover,
S-calculus lends itself to automation, i.e. the above-mentioned proofs can be automated by using
theorem provers. We will demonstrate those possibilities using the prover Coq [6][31].

2

The Basic Components

The basic components of the S-calculus are:
1.) The set of abstract states (abstract state space) A,
2.) State variables (S-variables) x, y, z, . . . ,
3.) State constants (S-constants) s1 , s2 , s3 , . . . ,
4.) S-predicates P, Q, R, . . . ,
5.) S-relations S1 , S2 , S3 , . . . ,
6.) S-formulas F1 , F2 , F3 , . . . ,
7.) Program variables a, b, c, . . . ,
8.) Program constants c1 , c2 , c3 , . . . ,
9.) The set of logical operations {¬, ∧, ∨, ⇒, ⇔}, where ¬ is negation, ∧ is conjunction, ∨ is
disjunction, ⇒ is implication and ⇔ is equivalence,
10.) Set of logical constants {⊤, ⊥} where ⊤ represents true and ⊥ represents false,
11.) Brackets ( ) and [ ] for changing the priority of operations.
Each S-constant describes an abstract state of the virtual machine. The set A of abstract
states is a set of all S-constants. S-predicates are logical functions over the abstract state space,
i.e. P : A → {⊤, ⊥}. Also, we need two special S-predicates τ and φ defined by
(T AU )
(P HI)

∀x ∈ A, τ (x) = ⊤,
∀x ∈ A, φ(x) = ⊥.

S-relations are relations on the abstract state space, i.e. S ⊆ A× A. In other words, S-relations
are logical functions on the set A × A, i.e. S : A × A → {⊤, ⊥}.
Definition 2.1 S-formulas are obtained in the following way:
a.) S-predicates and S-relations are S-formulas.
b.) If F1 and F2 are S-formulas then ¬F1 , F1 ∧F2 , F1 ∨F2 , F1 ⇒ F2 , F1 ⇔ F2 are also S-formulas.
c.) Any formula obtained from a.) and b.) in a finite number of steps is an S-formula.
Let {v1 , v2 , . . . , vn } be a set of program variables, which take values from sets D1 , D2 , . . . , Dn
respectively. Let A′ be a subset of A, with the cardinality Card(A′ ) = Card(D1 × D2 × · · · × Dn ).
Interpretation of the set A with respect to the set {v1 , v2 , . . . , vn } is a bijection that maps any
S-constant from A′ to the appropriate vector of program constants from D1 , D2 , . . . , Dn (usually
called state vector). S-relation S(x, y) contains ordered pairs (x, y), where x ∈ A is the initial state
and y ∈ A is the final state. Interpreted restriction of S-relation on the set A′ is called syntactic
unit on program variables {v1 , v2 , . . . , vn }. A syntactic unit may be written in many different ways

4

A. Kupusinac and D. Malbaški

(program code is one of them), and it can refer to a statement, block, subprogram or program.
We will use a term ”predicate” for an interpreted restriction of S-predicate on the set A′ , knowing
that it is actually a boolean expression over program variables {v1 , v2 , . . . , vn }. This means that we
observe two domains: the abstract state domain with S-constants, S-variables, S-predicates and
S-relations and the interpretation domain with vectors of program constants, program variables,
predicates and syntactic units. To simplify, S-constant is interpreted as a vector of program
constants from the set D1 , D2 , . . . , Dn , S-predicate is interpreted as a boolean expression, and
S-relation as a syntactic unit with program variables {v1 , v2 , . . . , vn }. Interpretation is denoted by
”:”. For example, x : a > 0 ∧ b = 5 means that S-variable x represents all states in which program
variables a and b satisfy a > 0 and b = 5.
The symbol ↔ means ”abbreviation”. If α is a token and F is an S-formula then α ↔ F means
”α is an abbreviation for F ”. If F1 and F2 are two S-formulas with the same form, we say that
F1 is syntactically identical to F2 , and write F1 = F2 . If F1 and F2 have the same meaning but
not the same form, they are semantically equivalent, denoted by F1 ≡ F2 .
S-calculus consists of S-formulas and is based solely on axioms and theorems of the first-order
predicate logic. It means that, among other things, the formulas {P }S{Q} and P {S}Q are just
two S-formulas:
a.) Total correctness formula (T CF ):
∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)))] .
b.) Partial correctness formula (P CF ):
∀x[(P (x) ∧ ∃yS(x, y)) ⇒ ∀z(S(x, z) ⇒ Q(z))] .
When writing S-formulas we will obey the usual priority conventions, where the order of priority
is: negation ¬, conjunction ∧, disjunction ∨, implication ⇒, equivalence ⇔. The priority can be
changed by using brackets ( ) and [ ].
Firstly, by using the formulas (T CF ) and (P CF ) we can formally define the total and partial
correctness of an S-relation with respect to S-predicates:
Definition 2.2 S-relation S is totally correct with respect to precondition P and postcondition Q
if the S-formula ∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)))] is valid.
Definition 2.3 S-relation S is partially correct with respect to precondition P and postcondition
Q if the S-formula ∀x[(P (x) ∧ ∃yS(x, y)) ⇒ ∀z(S(x, z) ⇒ Q(z))] is valid.
Hoare’s total correctness formula, denoted by {P }S{Q}, is defined by the statement ”if the
syntax unit S starts in a state satisfying the predicate P , then it terminates in a state satisfying the
predicate Q” [17]. The connection between this sentence and the formula (T CF ) is apparent: if
for every state x the S-predicate P holds, then the S-formula ∀x∃yS(x, y) ∧ ∀x∀z(S(x, z) ⇒ Q(z))
is true. The state x is then called the initial state. The formula ∀x∃yS(x, y) means that for every
initial state x there exists a state y such that (x, y) ∈ S. The state y is then called the final state.
The meaning of the S-formula ∀x∀z(S(x, z) ⇒ Q(z)) is the following: if for every initial state x
and every state z it is true that (x, z) ∈ S, then in the state z the S-predicate Q is true.
Hoare’s partial correctness formula, denoted by P {S}Q, is defined by the statement ”if the
syntax unit S starts in a state satisfying the predicate P and if it terminates then the final
state satisfies the predicate Q” [17]. In terms of the S-calculus, we assert: if for some state x
the predicate P holds and if there exists a final state y such that (x, y) ∈ S, then the formula
∀x∀z(S(x, z) ⇒ Q(z)) is true.
Concerning the question of indeterminism, S-calculus does not require any additional formulas
such as angelical or demonical formulas in refinement calculus [3], because the formulas (T CF ) and

S-Program Calculus

5

(P CF ) contain ∀x∀z(S(x, z) ⇒ Q(z)). Thus, S-calculus strictly implements Dijkstra’s statement
”Eventually I came to regard nondeterminacy as the normal situation, determinacy being reduced
to a - not even very interesting - special case” [14].
The S-calculus is a special kind of the first-order predicate logic or, more precisely, it is a
predicate logic over S-formulas. Its axiomatic system consists solely of the predicate logic axioms,
provided that formulas F , G and H are now S-formulas:
(A1 )
(A2 )
(A3 )
(A4 )
(A5 )

F ⇒ (G ⇒ F )
(F ⇒ (G ⇒ H)) ⇒ ((F ⇒ G) ⇒ (F ⇒ H))
(¬F ⇒ ¬G) ⇒ (G ⇒ F )
∀xF (x) ⇒ F (t) (term t is free for x in F (t))
∀x(F ⇒ G) ⇒ (F ⇒ ∀xG) (variable x is not free in F )

The S-calculus uses the rules of inference from the first-order predicate logic (the symbols F
and G stand for S-formulas):
a.) Modus ponens (M P N ):
F, F ⇒ G
G
b.) Generalisation (GEN ) :
F
∀xF
All theorems i.e. valid formulas in predicate logic are also valid in the S-calculus and vice versa.
We will briefly cite some well-known theorems of predicate logic that will be needed for further
proofs in this paper (again, the symbols F , G, H and K stand for S-formulas and τ and φ are
defined by (T AU ) and (P HI) respectively):
(T1 )
(T2 )
(T3 )
(T4 )
(T5 )
(T6 )
(T7 )
(T8 )
(T9 )
(T10 )
(T11 )
(T12 )
(T13 )
(T14 )
(T15 )
(T16 )
(T17 )
(T18 )
(T19 )
(T20 )
(T21 )
(T22 )

∀x∀yF ⇔ ∀y∀xF
∃x∀yF ⇒ ∀y∃xF
∀xF ⇔ F
∀x(F ∧ G) ⇔ ∀xF ∧ ∀xG
∀xF ∨ ∀xG ⇒ ∀x(F ∨ G)
¬∀xF ⇔ ∃x¬F
∀xF ⇔ ∀x(F ⇔ τ )
∀x(τ ⇒ F ) ⇔ ∀xF
∀x¬F ⇔ ∀x(F ⇔ φ)
∀x(F ⇔ F ∧ F )
∀x(F ⇔ F ∨ G)
∀x(¬F ∨ ¬G) ⇔ ∀x¬(F ∧ G)
∀x(¬F ∧ ¬G) ⇔ ∀x¬(F ∨ G)
∀x(F ⇒ G) ⇒ (∀xF ⇒ ∀xG)
∀x(F ⇒ G) ⇔ ∀x(¬F ∨ G)
∀x[(F ⇒ H) ∧ (H ⇒ G)] ⇒ ∀x(F ⇒ G)
∀x[(F ⇒ G) ∧ (H ⇒ K)] ⇒ ∀x[(F ∨ H) ⇒ (G ∨ K)]
∀x[(F ⇒ G) ∧ (H ⇒ K)] ⇒ ∀x[(F ∧ H) ⇒ (G ∧ K)]
∀x[(F ⇒ G) ∧ (F ⇒ H)] ⇔ ∀x(F ⇒ G ∧ H)
∀x[(F ⇒ G) ∧ (F ⇒ H)] ⇔ ∀x(F ⇒ G ∨ H)
∀x[(F ⇒ H) ∧ (G ⇒ H)] ⇔ ∀x(F ∨ G ⇒ H)
∀x[(F ⇒ G) ∨ (H ⇒ K)] ⇒ ∀x[(F ∧ H) ⇒ (G ∨ K)]

Program correctness or a new S-calculus theorem are proven by proving the validity of an
appropriate S-formula. This needs a modest mathematical apparatus e.g. the axioms, theorems

6

A. Kupusinac and D. Malbaški

and proof procedures of the first-order predicate logic. Moreover, it can be automated using various
automatic theorem provers.
An important detail is also the fact that the S-calculus is based on the abstract set of states
A. This means that when applying the Hoare logic we do not need an exact description of every
abstract state, thus avoiding the use of the program state vector (vector of all program variables).
It is known that the use of state vector introduces certain difficulties, since it is not quite clear
how to model unknown values of program variables [14]. In addition, the state vector is associated
with the specific program, and can not be related to the virtual machine when the program is not
active. Subprograms also contribute to the problem because they have their own state vectors.
On the other hand, the abstract state space is associated with the virtual machine itself so it is
always meaningful, regardless of whether a particular program is active or not. In the S-calculus
the program state space A′ is a subset of the virtual machine abstract state space A (A′ ⊆ A), and
every program is a restriction on A′ of the appropriate S-relation where S ⊆ A × A.

3

General Laws of the Hoare logic

In this section we will consider the general laws of Hoare logic [1][17] such as the laws of consequence,
disjunction, conjunction and negation. While the Hoare logic treats these laws as rules, we will
treat them as theorems. Some of them will be proven using Coq automatic prover.
Theorem 3.1 (Laws of Consequence) The following S-formulas are valid:
a.) ∀x(P (x) ⇒ R(x)) ∧ {R}S{Q} ⇒ {P }S{Q},
b.) {P }S{R} ∧ ∀x(R(x) ⇒ Q(x)) ⇒ {P }S{Q},
c.) ∀x(U (x) ⇒ P (x)) ∧ ∀x(Q(x) ⇒ V (x)) ∧ {P }S{Q} ⇒ {U }S{V }.
Proof.
a.) Since:
{R}S{Q} ↔ ∀x[R(x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)))],
the left side of the implication can be written as:
∀x(P (x) ⇒ R(x)) ∧ ∀x[R(x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)))]
and by the Theorem (T16 ), we obtain:
∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)))],
i.e.
{P }S{Q}.
b.) Since:
{P }S{R} ↔ ∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ R(z)))],
the left side of the implication can be written as:
∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ R(z)))] ∧ ∀x(R(x) ⇒ Q(x))
and by the Theorem (T16 ), we obtain:
∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)))],
i.e.
{P }S{Q}.
c.) By the Theorem 3.1.a.), the left side of the implication can be written as:
∀x(Q(x) ⇒ V (x)) ∧ {U }S{Q}
and by the Theorem 3.1.b.), we obtain:
{U }S{V }.


S-Program Calculus

7

The Theorems 3.1 also can be proven using automatic prover Coq (Appendix A). Finally, using
by the Theorem (T3 ), from Theorems 3.1 we can obtain the well-known Hoare’s rules of consequence [1][17]:
(P ⇒ R), {R}S{Q}
,
{P }S{Q}

{P }S{R}, (R ⇒ Q)
{P }S{Q}

and

(U ⇒ P ), (Q ⇒ V ), {P }S{Q}
.
{U }S{V }

Theorem 3.2 (Laws of Conjunction) The following S-formulas are valid:
a.) {P }S{Q} ∧ {R}S{W } ⇒ {P ∨ R}S{Q ∨ W },
b.) {P }S{Q} ∧ {R}S{W } ⇒ {P ∧ R}S{Q ∧ W }.
Proof.
a.) Since:
{P }S{Q} ↔ ∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)))],
{R}S{W } ↔ ∀x[R(x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ W (z)))],
by the Theorem (T17 ), the left side of the implication can be written as:
∀x[(P (x) ∨ R(x)) ⇒ ((∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))) ∨ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ W (z))))]
≡ ∀x[(P (x) ∨ R(x)) ⇒ ∃y((S(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))) ∨ (S(x, y) ∧ ∀z(S(x, z) ⇒ W (z))))]
≡ ∀x[(P (x) ∨ R(x)) ⇒ ∃yS(x, y) ∧ ∀z((S(x, z) ⇒ Q(z)) ∨ (S(x, z) ⇒ W (z)))].
Then, by the Theorem (T15 ), we obtain:
∀x[(P (x) ∨ R(x)) ⇒ ∃yS(x, y) ∧ ∀z(¬S(x, z) ∨ Q(z) ∨ ¬S(x, z) ∨ W (z))]
≡ ∀x[(P (x) ∨ R(x)) ⇒ ∃yS(x, y) ∧ ∀z(¬S(x, z) ∨ Q(z) ∨ W (z))]
and after that, by the Theorem (T15 ), we obtain:
∀x[(P (x) ∨ R(x)) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ (Q(z) ∨ W (z)))],
i.e.
{P ∨ R}S{Q ∨ W }.
b.) By the Theorem (T18 ), the left side of the implication can be written as:
∀x[(P (x) ∧ R(x)) ⇒ ((∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))) ∧ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ W (z))))]
≡ ∀x[(P (x) ∧ R(x)) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)) ∧ ∀z(S(x, z) ⇒ W (z)))]
≡ ∀x[(P (x) ∧ R(x)) ⇒ ∃yS(x, y) ∧ ∀z((S(x, z) ⇒ Q(z)) ∧ (S(x, z) ⇒ W (z)))]
and by the Theorem (T19 ), we obtain:
∀x[(P (x) ∧ R(x)) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ (Q(z) ∧ W (z)))],
i.e.
{P ∧ R}S{Q ∧ W }.

Colorallary 3.1 (Law of Resolution) The following S-formula is valid:
{P }S{Q} ∧ {¬P }S{W } ⇒ {τ }S{Q ∨ W }.
Proof.
If we substitute R with ¬P in the Theorem 3.2.a.) we obtain:
{P }S{Q} ∧ {¬P }S{W } ⇒ {P ∨ ¬P }S{Q ∨ W },
i.e.
{P }S{Q} ∧ {¬P }S{W } ⇒ {τ }S{Q ∨ W }.


8

A. Kupusinac and D. Malbaški

Theorem 3.3 (Laws of Disjunction) The following S-formula is valid:
{P }S{Q} ∨ {R}S{W } ⇒ {P ∧ R}S{Q ∨ W }.
Proof.
Since:
{P }S{Q} ↔ ∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)))],
{R}S{W } ↔ ∀x[R(x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ W (z)))],
by the Theorem (T22 ), the left side of implication can be written as:
∀x[(P (x) ∧ R(x)) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))) ∨ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ W (z)))]
≡ ∀x[(P (x) ∧ R(x)) ⇒ ∃yS(x, y) ∧ ∀z((S(x, z) ⇒ Q(z)) ∨ (S(x, z) ⇒ W (z)))]
and by the Theorem (T20 ), we obtain:
∀x[(P (x) ∧ R(x)) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ (Q(z) ∨ W (z)))],
i.e.
{P ∧ R}S{Q ∨ W }.

The proves of Theorems 3.2.a), 3.2.b) and 3.3 in Coq are given in Appendix A.
Theorem 3.4 (Laws of Conjunction and Disjunction) The following S-formulas are valid:
a.) {P ∨ R}S{Q} ⇔ {P }S{Q} ∧ {R}S{Q},
b.) {P }S{Q ∧ R} ⇔ {P }S{Q} ∧ {P }S{R},
c.) {P ∨ U }S{Q ∧ W } ⇔ {P }S{Q} ∧ {U }S{W } ∧ {P }S{W } ∧ {U }S{Q},
d.) {P }S{Q} ∨ {P }S{W } ⇒ {P }S{Q ∨ W }.
Proof.
a.) The left side of the eqivalence can be written as:
∀x[(P (x) ∨ R(x)) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))]
and by the Theorem (T21 ), we obtain:
∀x[(P (x) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))) ∧ (R(x) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)))],
i.e.
{P }S{Q} ∧ {R}S{Q}.
b.) The left side of the eqivalence can be written as:
∀x[P (x) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ (Q(z) ∧ R(z)))].
Then, by the Theorem (T19 ), we obtain:
∀x[P (x) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)) ∧ ∀z(S(x, z) ⇒ R(z))]
and after that, by the Theorem (T10 ), we obtain:
∀x[P (x) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)) ∧ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ R(z))]
and finally, by the Theorem (T19 ), we obtain:
∀x[P (x) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))] ∧ ∀x[P (x) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ R(z))],
i.e.
{P }S{Q} ∧ {P }S{R}.
c.) By the Theorem 3.4.a.), from the left side of the equivalence we obtain:
{P ∨ U }S{Q ∧ W } ⇔ {P }S{Q ∧ W } ∧ {U }S{Q ∧ W }
and by the Theorem 3.4.b.), we obtain:
{P }S{Q ∧ W } ∧ {U }S{Q ∧ W } ⇔ {P }S{Q} ∧ {U }S{W } ∧ {P }S{W } ∧ {U }S{Q}.

S-Program Calculus

d.) If we substitute R with P in the Theorem 3.3 we obtain:
{P }S{Q} ∨ {P }S{W } ⇒ {P ∧ P }S{Q ∨ W }
and by the Theorem (T10 ), we obtain:
{P }S{Q} ∨ {P }S{W } ⇒ {P }S{Q ∨ W }.

Theorem 3.5 (General Law of the Excluded Miracle) The following S-formula is valid:
{P }S{φ} ⇔ (P ⇔ φ), i.e. {P }S{φ} ⇔ ¬P .
Proof.
The left side of the equivalence can be written as:
∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ φ(z)))].
Since the S-formula ∀x∀z(S(x, z) ⇒ φ(z)) is valid if ∀x∀z¬S(x, z) is valid, we obtain:
∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z¬S(x, z))]
≡ ∀x[P (x) ⇒ φ(x)]
and by the Theorem (T9 ), we obtain:
∀x¬P (x),
i.e.
¬P .

Theorem 3.6 (Laws of Negation) The following S-formulas are valid:
a.) {P }S{Q} ∧ {R}S{¬Q} ⇒ ¬(P ∧ R),
b.) {P }S{Q} ∧ {P }S{¬Q} ⇔ ∀x¬P (x),
c.) [{P }S{¬Q} ⇒ ¬{P }S{Q}] ⇔ ∃xP (x),
d.) {P }S{Q} ∧ {¬P }S{Q} ⇔ ∀x∃yS(x, y) ∧ ∀x∀z(S(x, z) ⇒ Q(x)),
e.) ∃x∃zS(x, z) ∧ ¬Q(z) ⇒ [{¬P }S{Q} ⇒ ¬{P }S{Q}].
Proof.
a.) If we substitute W with ¬Q in the Theorem 3.2.b.), we obtain:
{P }S{Q} ∧ {R}S{¬Q} ⇒ {P ∧ R}S{Q ∧ ¬Q}
≡ {P }S{Q} ∧ {R}S{¬Q} ⇒ {P ∧ R}S{φ}
and by the Theorem 3.5, we obtain:
{P }S{Q} ∧ {R}S{¬Q} ⇒ ¬(P ∧ R).
b.) If we substitute R with ¬Q in the Theorem 3.4.b.), we obtain:
{P }S{Q} ∧ {P }S{¬Q} ⇔ {P }S{Q ∧ ¬Q}
≡ {P }S{Q} ∧ {P }S{¬Q} ⇔ {P }S{φ}
and by the Theorem 3.5, we obtain:
{P }S{Q} ∧ {P }S{¬Q} ⇔ ¬P ,
i.e.
{P }S{Q} ∧ {P }S{¬Q} ⇔ ∀x¬P (x).

9

10

A. Kupusinac and D. Malbaški

c.) By the Theorem (T15 ), the left side of the equivalence become:
¬{P }S{¬Q} ∨ ¬{P }S{Q}
and subsequently, by the Theorem (T12 ), we obtain:
¬[{P }S{¬Q} ∧ {P }S{Q}].
Then, by the Theorem 3.6.b.), we obtain:
¬[∀x¬P (x)]
and after that, by the Theorem (T6 ), we obtain:
∃xP (x).
d.) If we substitute R with ¬P in the Theorem 3.4.a.), we obtain:
{P ∨ ¬P }S{Q}
≡ {τ }S{Q}.
Since:
{τ }S{Q} ↔ ∀x[τ (x) ⇒ ∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))],
by the Theorem (T8 ), we obtain:
∀x[∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))].
e.) By the Theorem (T15 ), the right side of the equivalence can be written as:
¬{¬P }S{Q} ∨ ¬{P }S{Q}
and by the Theorem (T12 ), we obtain:
¬[{¬P }S{Q} ∧ {P }S{Q}].
Then, by the Theorem 3.6.d.), we obtain:
¬∀x[∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))]
≡ ∃x¬[∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z))].
By the Theorem (T13 ), we obtain:
∃x[¬∃yS(x, y) ∨ ¬∀z(S(x, z) ⇒ Q(z))]
≡ ∃x[∀y¬S(x, y) ∨ ∃z¬(S(x, z) ⇒ Q(z))]
and by the Theorem (T15 ), we obtain:
∃x[∀y¬S(x, y) ∨ ∃z¬(¬S(x, z) ∨ Q(z))].
After that, by the Theorem (T12 ), we obtain:
∃x[∀y¬S(x, y) ∨ ∃z(S(x, z) ∧ ¬Q(z))]
≡ ∃x∀y¬S(x, y) ∨ ∃x∃z(S(x, z) ∧ ¬Q(z))
and finally, by the Theorem (T11 ), we obtain:
∃x∃z(S(x, z) ∧ ¬Q(z)) ⇒ ∃x∃z(S(x, z) ∧ ¬Q(z)) ∨ ∃x∀y¬S(x, y).

The proves of Theorems 3.5, 3.6.a) and 3.6.b) in Coq are given in Appendix A.
Colorallary 3.2 The following S-formula is valid:
{P }S{Q} ∧ {P }S{¬Q} ⇔ (P ⇔ φ).
Proof.
From the Theorem 3.6.b.) we obtain:
∀x¬P (x),
i.e.
(P ⇔ φ).


S-Program Calculus

11

Colorallary 3.3 The following S-formula is valid:
[{P }S{¬Q} ⇒ ¬{P }S{Q}] ⇔ ¬(P ⇔ φ).
Proof.
From Theorem 3.6.c.) we obtain:
∃xP (x)
≡ ¬(∀x¬P (x)),
i.e.
¬(P ⇔ φ).


4

Special S-Relations

In Hoare logic, the so-called special syntax units such as if-then, if-then-else, while etc. are introduced by rules, whilst the assignment is defined through an axiom [1][17]. In the S-calculus, things
are different, since all special syntax units are treated as particular S-formulas. In other words,
for every syntax unit we define an appropriate S-relation that is a subset of the set A × A where A
is the abstract state space. We will discuss the meaning of this on the example of assignment. Let
a be a program variable of the type integer. The syntax unit a := 5; is an interpretation of the
S-relation Sa:=5; , which transfers the virtual machine from the state x to the state y. The state x
is interpreted as a state in which the variable a has some value from the its domain Dinteger (i.e.
a ∈ Dinteger ), and the state y is interpreted as a state in which the variable a has the value 5 (i.e.
a = 5). Accordingly, we define the S-relation Sa:=5; as a set of ordered pairs (x, y), x, y ∈ A where
x : a ∈ Dinteger and y : a = 5, or as an S-formula ∀x∀ySa:=5; (x, y) ⇔ x : a ∈ Dinteger ∧ y : a = 5.
Let x, y, y1 , y2 , . . . , yn , z ∈ A, where A is abstract state set and let a be a program variable of
the type T ype. The definitions of special S-relations no-operation, assignment, if-then-else, if-then,
sequence and while are as follows:

Definition 4.1 (No-operation) S-relation Snop is defined as:
a.) set Snop = {(x, y)|x = y}, or
b.) S-formula ∀x∀ySnop (x, y) ⇔ x = y.
Definition 4.2 (Assignment) S-relation Sa:=e; is defined as:
a.) set Sa:=e; = {(x, y)|x : a ∈ DT ype ∧ y : a = e}, or
b.) S-formula ∀x∀ySa:=e; (x, y) ⇔ x : a ∈ DT ype ∧ y : a = e.
Definition 4.3 (If-then-else) S-relation Sif −then−else is defined as:
a.) set Sif −then−else = {(x, y)|(B(x) ∧ S1 (x, y)) ∨ (¬B(x) ∧ S2 (x, y))}, or
b.) S-formula ∀x∀ySif −then−else (x, y) ⇔ (B(x) ∧ S1 (x, y)) ∨ (¬B(x) ∧ S2 (x, y)).
Definition 4.4 (If-then) S-relation Sif −then is defined as:
a.) set Sif −then = {(x, y)|(B(x) ∧ S(x, y)) ∨ (¬B(x) ∧ Snop (x, y))}, or
b.) S-formula ∀x∀ySif −then (x, y) ⇔ (B(x) ∧ S(x, y)) ∨ (¬B(x) ∧ Snop (x, y)).

12

A. Kupusinac and D. Malbaški

Definition 4.5 (Sequence) S-relation S[S1 ;S2 ] is defined as:
a.) set S[S1 ;S2 ] = {(x, y)|∃z(S1 (x, z) ∧ S2 (z, y))}, or
b.) S-formula ∀x∀yS[S1 ;S2 ] (x, y) ⇔ ∃z(S1 (x, z) ∧ S2 (z, y)).
Definition 4.6 (While) S-relation Swhile is defined as:
a.) set Swhile = {(x, y)|∃y1 , y2 , . . . , yn B(x) ∧ S(x, y1 ) ∧ B(y1 ) ∧ S(y1 , y2 ) ∧ B(y2 ) ∧ S(y2 , y3 ) ∧
· · · ∧ B(yn ) ∧ S(yn , y) ∧ ¬B(y)}, or
b.) S-formula ∀x∀ySwhile (x, y) ⇔ ∃y1 , y2 , . . . , yn B(x) ∧ S(x, y1 ) ∧ B(y1 ) ∧ S(y1 , y2 ) ∧ B(y2 ) ∧
S(y2 , y3 ) ∧ · · · ∧ B(yn ) ∧ S(yn , y) ∧ ¬B(y).
In the previous section, the theorems that represent the general laws of Hoare logic were proven.
In this section, the special syntax units were analyzed using S-relations introduced by the appropriate definitions. In this way, we have developed a mechanism for proving the correctness of
syntax units with respect to the specification given. Every syntax unit is treated as an interpretation of the appropriate S-relation, and the program specification is modeled as an ordered pair
of S-predicates (P, Q), where P is a precondition and Q is a postcondition. Apparently, proving
syntax unit correctness conforms to proving the validity of the appropriate S-formula containing
S-relation S and S-predicates P and Q. In addition to generality, one of the main advantages of
this approach is simplicity, because the proof procedures do not require complicated mathematical
apparatus. In order to prove program correctness and/or a new theorem it is sufficient to know
first-order predicate calculus.
Various theories related to program semantics description and analysis that use an interpreted
set of states do not deal with variable declarations. The reason is that they use the vector of
program variables to describe states, so the problem arises of how to deal with state descriptions
when some program variables are not (yet) defined. Such a problem does not exist in the Scalculus because it relies on the abstract state space. For defining a variable declaration, we use
an appropriate S-relation defined by:
Definition 4.7 (Declaration) S-relation Sa:T ype; is defined as:
a.) set Sa:T ype; = {(x, y)|y : a ∈ DT ype }, or
b.) S-formula ∀x∀ySa:T ype; (x, y) ⇔ y : a ∈ DT ype .
The possibility of modeling variable declaration is of considerable importance, especially for
languages where declaration is treated as an ordinary statement (as in C/C++), and even may
appear anywhere in the source code (as in Java). Using the appropriate S-relation enables us to
automate verification of such programs. Let us consider simple two programs written in C.

4.1

Example

Is the syntax unit written in C and given in Figure 1 correct with respect to the specification given
as a pair of predicates (⊤, a = 10)?
The given syntax unit is an interpretation of S-relation S:
S : a : integer; a := 5; if a > 0 then a := 10 else a := 100;
The specification is an ordered pair of S-predicates (P, Q) where the precondition is P : ⊤
and the postcondition is Q : a = 10. Now, we have to prove the validity of the S-formula
{P }S{Q} ↔ ∀x[P (x) ⇒ (∃yS(x, y) ∧ ∀z(S(x, z) ⇒ Q(z)))]. Apart from P , S and Q, we will use

S-Program Calculus

13
int a=5;
if (a > 0)
a=10;
else
a=100;
Figure 1: Example 4.1

the following notation:
S1 : a : integer;
S2 : a := 5; if a > 0 then a := 10 else a := 100;
S3 : a := 5;
S4 : if a > 0 then a := 10 else a := 100;
S5 : a := 10;
S6 : a := 100;
R : a ∈ Dinteger
T : a=5
B: a>0
W : a = 10
U : a = 100
We will prove total correctness of the S-relation S with respect to the specification (τ, W ),
i.e. we will prove that the formula {τ }S{W } is valid. The S-relation S is a sequence [S1 ; S2 ].
Consequently, according to the Definition 4.5, the following formula is valid:
∀x∀yS(x, y) ⇔ ∃zS1 (x, z) ∧ S2 (z, y).

(1)

Further, we prove that the S-relation S1 is totally correct with respect to the specification
(τ, R). Since S1 is declaration of the program variable a : integer, according to the Definition 4.7,
the following S-formulas are valid:
∀x∀yS1 (x, y) ⇔ y : a ∈ Dinteger ,
{τ }S1 {R}.

(2)
(3)

We proceed by proving that the S-relation S2 is correct with respect to the specification (R, W ),
i.e. that the S-formula {R}S{W } is valid. The S-relation S2 is sequence [S3 ; S4 ]. According to
the Definition 4.5, it follows that the S-formula
∀x∀yS2 (x, y) ⇔ ∃zS3 (x, z) ∧ S4 (z, y)

(4)

is valid. The S-relation S3 is assignment. According to the Definition 4.2, the following formulas
are valid:
∀x∀zS3 (x, z) ⇔ x : a ∈ Dinteger ∧ z : a = 5,
{R}S3 {T },
B(z).

(5)
(6)
(7)

The S-relations S5 and S6 are assignments. From the Definition 4.2, it follows that the formulas
(8) - (11) are also valid:

14

A. Kupusinac and D. Malbaški
while (i <= n) {
f*=i;
i++;
}
Figure 2: Example 4.2

∀z∀yS5 (z, y) ⇔ z : a ∈ Dinteger ∧ y : a = 10,
{R}S5 {W },
∀z∀yS6 (z, y) ⇔ z : a ∈ Dinteger ∧ y : a = 100,
{R}S6 {U }.

(8)
(9)
(10)
(11)

Since T ⇒ R, by the Theorem 3.1.a.), the following formulas are valid:
{T }S5{W },
{T }S6{U }.

(12)
(13)

The S-relation S4 is if-then-else so, by the Definition 4.3, the following formula is valid:
∀z∀yS4 (z, y) ⇔ (B(z) ∧ S5 (z, y)) ∨ (¬B(z) ∧ S6 (z, y)).

(14)

From (7), (12) and (14) we infer the validity of the formula:
{T }S4{W }.

(15)

From (4), (6) and (15) we conclude:
{R}S2 {W }.

(16)

From (1), (3) and (16) we conclude:
{τ }S{W }.
Since P ⇒ τ and W ⇒ Q, from the Theorem 3.1.c.) we conclude that the formula
{P }S{Q}
is valid, Q.E.D.

4.2

Example

Is the syntax unit written in C and given in Figure 2 correct with respect to the specification given
as a pair of predicates (i = 2 ∧ n = 4 ∧ f = 1, f = 24)?
The given syntax unit is an interpretation of S-relation S:
S : while i <= n do begin f := f ∗ i; i := i + 1; end;
We have to prove the validity of {P }S{Q}, where P : i = 2 ∧ n = 4 ∧ f = 1 and Q : f = 24.
Apart from S, P and Q, we will use the following notation:

S-Program Calculus

R:
B:
S1 :
S2 :
S3 :

15

i = 5 ∧ n = 4 ∧ f = 24
i <= n
f := f ∗ i; i := i + 1;
f := f ∗ i;
i := i + 1;

According to the Definition 4.2, the following formulas are valid:
∀x∀z1 S2 (x, z1 ) ⇔ x : i = 2 ∧ n = 4 ∧ f = 1 ∧ z1 : i = 2 ∧ n = 4 ∧ f = 2,
∀z1 ∀y1 S3 (z1 , y1 ) ⇔ z1 : i = 2 ∧ n = 4 ∧ f = 2 ∧ y1 : i = 3 ∧ n = 4 ∧ f = 2
and by the Definition 4.5, we obtain:
∀x∀y1 S1 (x, y1 ) ⇔ x : i = 2 ∧ n = 4 ∧ f = 1 ∧ y1 : i = 3 ∧ n = 4 ∧ f = 2.

(17)

From the S-formula (17) we conclude that the following formulas are valid:
∀xB(x),
∀y1 B(y1 ).

(18)
(19)

According to the Definition 4.2, the following formulas are valid:
∀y1 ∀z2 S2 (y1 , z2 ) ⇔ y1 : i = 3 ∧ n = 4 ∧ f = 2 ∧ z2 : i = 3 ∧ n = 4 ∧ f = 6,
∀z2 ∀y2 S3 (z2 , y2 ) ⇔ z2 : i = 3 ∧ n = 4 ∧ f = 6 ∧ y2 : i = 4 ∧ n = 4 ∧ f = 6
and by the Definition 4.5, we obtain:
∀y1 ∀y2 S1 (y1 , y2 ) ⇔ y1 : i = 3 ∧ n = 4 ∧ f = 2 ∧ y2 : i = 4 ∧ n = 4 ∧ f = 6.

(20)

From the S-formula (20) we conclude that the following formula is valid:
∀y2 B(y2 ).

(21)

According to the Definition 4.2, the following formulas are valid:
∀y2 ∀z3 S2 (y2 , z3 ) ⇔ y2 : i = 4 ∧ n = 4 ∧ f = 6 ∧ z3 : i = 4 ∧ n = 4 ∧ f = 24,
∀z3 ∀yS3 (z3 , y) ⇔ z3 : i = 4 ∧ n = 4 ∧ f = 24 ∧ y : i = 5 ∧ n = 4 ∧ f = 24
and by the Definition 4.5, we obtain:
∀y2 ∀yS1 (y2 , y) ⇔ y2 : i = 4 ∧ n = 4 ∧ f = 6 ∧ y : i = 5 ∧ n = 4 ∧ f = 24.

(22)

From the S-formula (22) we conclude that the following formula is valid:
∀y¬B(y).
From the S-formulas (17) - (23) we conclude that the following formula is valid:
∀x∀yS(x, y) ⇔ ∃y1 , y2 B(x) ∧ S1 (x, y1 ) ∧ B(y1 ) ∧ S1 (y1 , y2 ) ∧ B(y2 ) ∧ S1 (y2 , y) ∧ ¬B(y)
and conclude that the following formula is valid:

(23)

16

A. Kupusinac and D. Malbaški

{P }S{R}.
Since R ⇒ Q, from the Theorem 3.1.b.) we conclude that the formula
{P }S{Q}
is valid, Q.E.D.

5

Proofs of Dijkstra’s Theorems on the Weakest Precondition

In the previous two sections, we have shown how to apply the S-calculus to prove program correctness. In this section, we will demonstrate the use of S-calculus for proving general theorems
in a strictly formal way. As an example, we will consider Dijkstra’s theorems on the weakest precondition wp, namely the laws of the excluded miracle, monotonicity, conjunction and disjunction.
While being correct, the original proofs [14][18] are not strictly formal, so our task will be to provide full formalization. In addition, we will establish yet another general law, the law of negation
(Theorem 5.5), in order to provide a more complete insight to the behavior of the operator wp.
The section ends with the formal proof of Dijkstra’s theorem on total correctness. Some of the
above-mentioned theorems will be proven in Coq.
Definition 5.1 (The Weakest Precondition) The weakest precondition of S-relation S with
respect to postcondition Q is S-predicate wp(S, Q) if:
(W P1 )
{wp(S, Q)}S{Q},
(W P2 )
{P }S{Q} ⇒ ∀x(P (x) ⇒ wp(S, Q)(x)).

Theorem 5.1 (Dijkstra’s Law of the Excluded Miracle) The following S-formula is valid:
wp(S, φ) ⇔ φ.
Proof.
According to (W P1 ) in the Definition 5.1, we obtain:
{wp(S, φ)}S{φ}
and by the Theorem 3.5, we conclude that the following formula is valid:
wp(S, φ) ⇔ φ.

Theorem 5.2 (Dijkstra’s Law of Monotonicity) The following S-formula is valid:
(Q ⇒ R) ⇒ (wp(S, Q) ⇒ wp(S, R)).
Proof.
According to (W P1 ) in the Definition 5.1, we obtain:
{wp(S, Q)}S{Q}
and by the Theorem 3.1.b.) we conclude that the following formula is valid:
{wp(S, Q)}S{Q} ∧ ∀x(Q(x) ⇒ R(x)) ⇒ {wp(S, Q)}S{R}.

S-Program Calculus

According to (W P2 ) in the Definition 5.1, we obtain:
(3) wp(S, Q) ⇒ wp(S, R).

Theorem 5.3 (Dijkstra’s Law of Conjunction) The following S-formula is valid:
wp(S, Q) ∧ wp(S, R) ⇔ wp(S, Q ∧ R).
Proof.
First, let us prove the left-right implication:
wp(S, Q) ∧ wp(S, R) ⇒ wp(S, Q ∧ R).
According to (W P1 ) in the Definition 5.1, we obtain the following S-formulas:
{wp(S, Q)}S{Q},
{wp(S, R)}S{R}.
By the Theorem 3.2.b.), we obtain:
{wp(S, Q)}S{Q} ∧ {wp(S, R)}S{R} ⇒ {wp(S, Q) ∧ wp(S, R)}S{Q ∧ R}
and according to (W P2 ) in the Definition 5.1, we obtain:
wp(S, Q) ∧ wp(S, R) ⇒ wp(S, Q ∧ R)
and conclude that the left-right implication is valid.
Further, let us prove the right-left implication:
wp(S, Q ∧ R) ⇒ wp(S, Q) ∧ wp(S, R).
According to (W P1 ) in the Definition 5.1, we obtain following S-formula:
{wp(S, Q ∧ R)}S{Q ∧ R}.
By the Theorem 3.4.b.), we obtain:
{wp(S, Q ∧ R)}S{Q} ∧ {wp(S, Q ∧ R)}S{R}
and according to (W P2 ) in the Definition 5.1, we obtain:
(wp(S, Q ∧ R) ⇒ wp(S, Q)) ∧ (wp(S, Q ∧ R) ⇒ wp(S, R)).
After that, by the Theorem (T19 ), we obtain:
wp(S, Q ∧ R) ⇒ wp(S, Q) ∧ wp(S, R)
and conclude that the right-left implication is valid.
Since both implications are valid, we conclude that the starting equivalence is valid.


Theorem 5.4 (Dijkstra’s Law of Disjunction) The following S-formula is valid:
wp(S, Q) ∨ wp(S, R) ⇒ wp(S, Q ∨ R).
Proof.
By the Theorem 3.2.a.), we obtain:
{wp(S, Q)}S{Q} ∧ {wp(S, R)}S{R} ⇒ {wp(S, Q) ∨ wp(S, R)}S{Q ∨ R}
and according to (W P2 ) in the Definition 5.1, we obtain:
wp(S, Q) ∨ wp(S, R) ⇒ wp(S, Q ∨ R).


17

18

A. Kupusinac and D. Malbaški

Theorem 5.5 (Law of Negation) The following S-formula is valid:
¬(wp(S, Q) ∧ wp(S, ¬Q)).
Proof.
According to (W P1 ) in the Definition 5.1, if we substitute P with wp(S, Q) and R with
wp(S, ¬Q) in the Theorem 3.6.a.), we obtain:
¬(wp(S, Q) ∧ wp(S, ¬Q).

Theorem 5.6 (Dijkstra’s Theorem on Total Correctness) The following S-formula is valid:
{P }S{Q} ⇔ (P ⇒ wp(S, Q)).
Proof.
First, let us prove the left-right implication:
{P }S{Q} ⇒ (P ⇒ wp(S, Q)).
According to (W P2 ) in the Definition 5.1, we conclude that the left-right implication is valid.
Further, let us prove the right-left implication:
(P ⇒ wp(S, Q)) ⇒ {P }S{Q}.
According to (W P1 ) in the Definition 5.1, we obtain following S-formula:
{wp(S, Q)}S{Q}.
If we substitute R with wp(S, Q) in the Theorem 3.1.a.), we obtain:
∀x(P (x) ⇒ wp(S, Q)(x)) ∧ {wp(S, Q)}S{Q} ⇒ {P }S{Q}
and conclude that the right-left implication is valid.
Since both implications are valid, we conclude that the starting equivalence is valid.

The proves of Theorems 5.1, 5.5 and 5.6 in Coq are given in Appendix A.

6

Conclusions

In this paper, we have developed the S-calculus, which represents a powerful mathematical tool
for program semantics analysis. The S-calculus is based on axioms and theorems of first-order
predicate logic and uses S-formulas, which are defined on the abstract state space of a virtual
machine. Proving program correctness and/or establishing new theorems conform to proving the
validity of the appropriate S-formula, and for that, we need only the first-order predicate logic.
Since the problem of indeterminism does not exist, S-calculus can consider total/partial correctness
without the need for additional concepts and formulas. Owing to its generality, the S-calculus can
cope with the semantics of variable declaration, where some other theories fail (the ones that are
based on the interpreted set of states).
The mathematical mechanism developed in this paper, apart from being general, brings together
Hoare’s ideas and first-order predicate logic. It also enables automatic proofs of program correctness
and/or new theorems. In this paper, we have provided strictly formal proofs for the general laws
of Hoare logic and Dijkstra’s theorems on the weakest precondition. Moreover, we have proven an
additional law related to the weakest precondition, namely the law of negation. As an example,
some of the theorems are proven using Coq automatic prover.
Our future research in the area of S-calculus will be aimed towards investigating more complex
properties and relationships that exist between preconditions, postconditions and syntax units,
especially in the object-oriented environment. The second line of work will be development of
algorithms for automated program correctness proofs, thus providing a practical aspect to Scalculus.

S-Program Calculus

19

References
[1] Apt, K. R. 1981. Ten Years of Hoares Logic: A Survey - Part I. ACM Transactions on
Programming Languages and Systems (TOPLAS) 3, 4 (October), 431-483.
[2] Arthan, R., Martin, U., Mathiesen, E. A., and Oliva, P. 2009. A general framework for sound
and complete Floyd-Hoare logics. ACM Transactions on Computational Logic (TOCL) 11, 1,
1-31.
[3] Back, R. J., Akademi, A., and von Wright, J. 1998. Refinement Calculus: A Systematic
Introduction. Springer-Verlag New York, Inc., Secaucus, NJ, USA.
[4] Back, R. J. and von Wright, J. 1992. Combining angels, demons and miracles in program
specifications. Theoretical Computer Science 100, 365-383.
[5] Backhouse, R. C. 1986. Program Construction and Verification. Prentice-Hall, Inc., Upper
Saddle River, NJ, USA.
[6] Bertot, Y. and Castéran, P. 2004. Interactive Theorem Proving and Program Development,
Coq’Art:the Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An
EATCS Series, vol. XXV. Springer-Verlag, Berlin, Heidelberg.
[7] Blass, A. and Gurevich, Y. 2000. The underlying logic of Hoare logic. Bull. of the Euro. Assoc.
for Theoretical Computer Science 70, 82-110.
[8] Church, A. 1941. The Calculi of Lambda Conversion. Princeton University Press, Princeton,
NJ, USA.
[9] Church, A. 1956. Introduction to Mathematical Logic. Vol. 1. Princeton University Press,
Princeton, NJ, USA.
[10] Cook, S. A. 1978. Soundness and completeness of an axiom system for program verification.
SIAM Jour. Comput. 7, 1 (February), 70-90.
[11] Curry, H. 1963. Foundations of Mathematical Logic. McGraw-Hill, New York, USA.
[12] Dahl, O. J., Dijkstra, E. W., and Hoare, C. A. R. 1972. Structured Programming. Academic
Press Ltd., London, UK, UK.
[13] de Bakker, J. W. 1980. Mathematical Theory of Program Correctness. Prentice-Hall, Inc.,
Upper Saddle River, NJ, USA.
[14] Dijkstra, E. W. 1976. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ, USA.
[15] Floyd, R. W. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer
Science, Proceedings of Symposia in Applied Mathematics. American Mathematical Society,
Providence, RI, USA, 19-32.
[16] Goldblatt, R. 1982. Axiomatising the Logic of Computer Programming. Springer-Verlag New
York, Inc., Secaucus, NJ, USA.
[17] Gordon, M. J. C. 1988. Programming Language Theory and its Implementation. Prentice Hall
International (UK) Ltd., Hertfordshire, UK, UK.
[18] Gries, D. 1987. The Science of Programming. Springer-Verlag New York, Inc., Secaucus, NJ,
USA.
[19] Hehner, E. C. R. 1984. Predicative programming. Communications of the ACM 27, 2, 134-151.

20

A. Kupusinac and D. Malbaški

[20] Hehner, E. C. R. 1999. Specifications, Programs, and Total Correctness. Science of Computer
Programming 34, 191-205.
[21] Hehner, E. C. R. 2009. A Practical Theory of Programming. Department of Computer Science,
University of Toronto, Canada, www.cs.utoronto.ca/∼hehner/aPToP.
[22] Hoare, C. A. R. 1969. An Axiomatic Basis for Computer Programming. Comunications of the
ACM 12, 10 (October), 576-585.
[23] Hoare, C. A. R. 1992. Programs are predicates. In Proceedings of the International Conference
on Fifth Generation Computer Systems (FGCS’92). Institute for New Generation Computer
Technology (ICOT, Ed.), Tokyo, Japan, 211-218.
[24] Hoare, C. A. R. and Roscoe, A. W. 1984. Programs as executable predicates. In Proceedings
of the International Conference on Fifth Generation Computer Systems (FGCS’84). Institute
for New Generation Computer Technology (ICOT, Ed.), Tokyo, Japan, 220-228.
[25] Kleene, S. C. 1967. Mathematical Logic. JohnWiley and Sons, Inc., New York, USA.
[26] Malbaški, D. and Kupusinac, A. 2009. Introduction to S-program calculus. Tech. Rep. 02121/128, Faculty of Technical Science, Novi Sad, Serbia.
[27] Nakano, M., Ogata, K., Nakamura, M., and Futatsugi, K. 2006. Automating invariant verification of behavioral specifications. In Proceedings of the Sixth International Conference on
Quality Software (QSIC’06). IEEE Computer Society, Beijing, China, 49-56.
[28] Pratt, V. R. 1976. Semantical Considerations on Floyd-Hoare logic. Tech. Rep. MIT/LCS/TR
168, Massachusetts Institute of Technology, Laboratory for Computer Science, Massachusett,
USA.
[29] Shoenfield, J. R. 1967. Mathematical Logic. Addison-Wesley Publishing Company, Reading,
MA, USA.
[30] Slonneger, K. and Kurtz, B. L. 1995. Formal Syntax and Semantics of Programming Languages. Addison-Wesley Publishing Company, Reading, MA, USA.
[31] The Coq Development Team. 2009. The Coq Proof Assistant Reference Manual Version 8.2bugfix. INRIA, Orsay, France.
[32] Zwiers, J. and Roever, W. 1989. Predicates are predicate transformers: a unified compositional
theory for concurrency. In Proceedings of the eighth annual ACM Symposium on Principles of
distributed computing (PODC’89, Edmonton, Alberta, Canada). ACM, New York, NY, USA,
265-279.

S-Program Calculus

A

21

Appendix

Theorem 3.1.a.):
Variable A: Set.
Variables P Q R: A->Prop.
Variable S: A->A->Prop.
Theorem t31a :
((forall x:A,(P x->R x)) /\
(forall x:A, (R x ->((exists y:A, S x y)/\(forall z:A, (S x z ->Q z )))))) ->
(forall x, (P x ->((exists y, S x y)/\(forall z, (S x z ->Q z ))))).
firstorder.

Theorem 3.1.b.):
Variable A: Set.
Variables P Q R: A->Prop.
Variable S: A->A->Prop.
Theorem t31b :
((forall x:A, (P x ->((exists y:A, S x y)/\(forall z:A, (S x z ->Q z ))))) /\
(forall z:A,(Q z->R z))) ->
(forall x, (P x ->((exists y, S x y)/\(forall z, (S x z ->R z ))))).
firstorder.

Theorem 3.1.c.):
Variable A: Set.
Variables P Q U V: A->Prop.
Variable S: A->A->Prop.
Theorem t31c :
((forall x:A,(U x->P x)) /\
(forall x:A, (P x ->((exists y:A, S x y)/\(forall z:A, (S x z ->Q z ))))) /\
(forall z:A,(Q z->V z))) ->
(forall x, (U x ->((exists y, S x y)/\(forall z, (S x z ->V z ))))).
firstorder.

Theorem 3.2.a.):
Variable A: Set.
Variables P R Q W: A->Prop.
Variable S: A->A->Prop.
Theorem t32a :
((forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->Q z ))))) /\
(forall x:A, (R x -> ((exists y:A, S x y)/\(forall z:A, (S x z->W z )))))) ->
(forall x:A, ((P x \/ R x) -> ((exists y:A, S x y)/\(forall z:A, (S x z->(Q z \/ W
z)))))).
firstorder.

22

A. Kupusinac and D. Malbaški

Theorem 3.2.b.):
Variable A: Set.
Variables P Q R W: A->Prop.
Variable S: A->A->Prop.
Theorem t32b :
((forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->Q z ))))) /\
(forall x:A, (R x -> ((exists y:A, S x y)/\(forall z:A, (S x z->W z )))))) ->
(forall x:A, ((P x /\ R x) -> ((exists y:A, S x y)/\(forall z:A, (S x z->(Q z /\ W
z)))))).
firstorder.

Theorem 3.3:
Variable A: Set.
Variables P Q R W: A->Prop.
Variable S: A->A->Prop.
Theorem t33 :
((forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->Q z ))))) \/
(forall x:A, (R x -> ((exists y:A, S x y)/\(forall z:A, (S x z->W z )))))) ->
(forall x:A, ((P x /\ R x) -> ((exists y:A, S x y)/\(forall z:A, (S x z->(Q z \/W
z)))))).
firstorder.

Theorem 3.5:
Variable A: Set.
Variables P : A->Prop.
Variable S: A->A->Prop.
Definition phi (x:A) := False.
Theorem t35 :
(forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->phi z)))) <->
(P x<->phi x)).
firstorder.

Theorem 3.6.a):
Variable A: Set.
Variables P Q R: A->Prop.
Variable S: A->A->Prop.
Theorem t36a :
((forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->Q z))))) /\
(forall x:A, (R x -> ((exists y:A, S x y)/\(forall z:A, (S x z->(∼Q z))))))) ->
(forall x:A, (∼(P x /\ R x))).
firstorder.

S-Program Calculus

23

Theorem 3.6.b):
Variable A: Set.
Variables P Q: A->Prop.
Variable S: A->A->Prop.
Theorem t36b :
((forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->Q z))))) /\
(forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->(∼Q z))))))) <->
(forall x:A, (∼(P x))).
firstorder.

Theorem 5.1:
Variable A: Set.
Variables P wpSphi: A->Prop.
Variable S: A->A->Prop.
Definition phi (x:A) := False.
Axiom wpSphi1 :
forall x:A, (wpSphi x -> ((exists y:A, S x y)/\(forall z:A, (S x z->phi z)))).
Axiom wpSphi2 :
forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->phi z)))) ->
(P x->wpSphi x).
Theorem t51 : forall x:A, (wpSphi x <-> phi x).
firstorder using wpSphi1 wpSphi2.

Theorem 5.5:
Variable A: Set.
Variables P Q R wpSQ wpSNQ: A->Prop.
Variable S: A->A->Prop.
Axiom wpSQ1 :
forall x:A, (wpSQ x -> ((exists y:A, S x y)/\(forall z:A, (S x z->Q z)))).
Axiom wpSQ2 :
forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->Q z)))) ->
(P x->wpSQ x).
Axiom wpSNQ1 :
forall x:A, (wpSNQ x -> ((exists y:A, S x y)/\(forall z:A, (S x z->(∼(Q z)))))).
Axiom wpSNQ2 :
forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->(∼(Q z)))))) ->
(P x->wpSNQ x).
Theorem t55 : forall x:A, (∼((wpSQ x)/\(wpSNQ x))).
firstorder using wpSQ1 wpSQ2 wpSNQ1 wpSNQ2.

24

A. Kupusinac and D. Malbaški

Theorem 5.6:
Variable A: Set.
Variables P Q wpSQ: A->Prop.
Variable S: A->A->Prop.
Axiom wpSQ1 :
forall x:A, (wpSQ x -> ((exists y:A, S x y)/\(forall z:A, (S x z->Q z)))).
Axiom wpSQ2 :
forall x:A, (P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->Q z)))) ->
(P x->wpSQ x).
Theorem t56 :
forall x:A, ((P x -> ((exists y:A, S x y)/\(forall z:A, (S x z->Q z)))) <->
((P x)->(wpSQ x))).
firstorder using wpSQ1 wpSQ2.

