Exercises in Nonstandard Static Analysis
of Hybrid Systems
Ichiro Hasuo1 and Kohei Suenaga2
1

University of Tokyo, Japan
Kyoto University, Japan

2

Abstract. In formal verification of hybrid systems, a big challenge is to incorporate continuous flow dynamics in a discrete framework. Our previous work proposed to use nonstandard analysis (NSA) as a vehicle from discrete to hybrid; andto verify hybrid systems using a Hoare logic. In this paper we aim to exemplify
the potential of our approach, through transferring static analysis techniques tohybrid applications. The transfer is routine via the transfer principle in NSA. The
techniques are implemented in our prototype automatic precondition generator.

1 Introduction
Hybrid systems exhibit both discrete (digital) jump and continuous (physical) flow dynamics. They are of paramount importance now that so many physical systems—cars,
airplanes, etc.—are controlled with computers. For an approach to hybrid systems fromthe formal verification community, the challenge is: 1) to incorporate flow-dynamics;
and 2) to do so at the lowest possible cost, so that the discrete framework smoothlytransfers to hybrid situations. A large body of existing work uses differential equations
explicitly in the syntax; see the discussion of related work below.
In [21], instead, we proposed to introduce a constant dt for an infinitesimal (i.e.
infinitely small) value, and turn flow into jump. With dt, the continuous operation of integration can be represented by a while-loop, to which existing discrete techniques suchas Hoare-style program logics readily apply. For a rigorous mathematical development
we employed nonstandard analysis (NSA) beautifully formalized by Robinson [15].
Concretely, in [21] we took the common triple of a W HILE-language, a first-orderassertion language and a Hoare logic (e.g. in the textbook [22]); and added a constant dt
to obtain a modeling and verification framework for hybrid systems. Its three components are called W HILEdt , A SSNdt and H OAREdt . These are connected by denotationalsemantics defined in the language of NSA. We proved soundness and relative completeness of the logic H OAREdt . Underlying the technical development is the idea of what
we call sectionwise execution, illustrated by the following example.
Example 1.1 Let celapse be the program on the right. The valueof dt is infinitesimal; therefore the while loop will not terminate
within finitely many steps. Nevertheless it is somehow intuitive to
expect that after an “execution” of this program, the value of t
should be infinitesimally close to 1.

t := 0 ;while t ≤ 1 do
t := t + dt

2

Our idea is to think about sectionwise execution. For each nat- t := 0 ;ural number i we consider the i-th section of the program celapse , while t ≤ 1 do
1denoted by celapse |i and shown on the right. Concretely, celapse |i ist := t + i+1
1. Inforobtained by replacing the infinitesimal dt in celapse with i+1
mally celapse |i is the “i-th approximation” of the original celapse .
1
A section celapse |i does terminate within finite steps and yields 1 + i+1
as the valueof t. Now we collect the outcomes of sectionwise executions and obtain a sequence( 1 + 1, 1 + 12 , 1 + 31 , . . . , 1 + 1i , . . . )(1)which is thought of as a progressive approximation of the actual outcome of the original
program celapse . Indeed, in the language of NSA, the sequence (1) represents a hyperreal
number r that is infinitesimally close to 1.
We note that a program in W HILEdt is not executable in general: the program celapse
executes infinitely many iterations. It is however a merit of static approaches to verification, that programs need not be executed to prove their correctness. Instead, welldefined mathematical semantics suffices and supports deductive reasoning. This is what
we do, with the denotational semantics of W HILEdt exemplified in Example 1.1.
This paper is a first step towards serious use of our framework of [21]. We employ various discrete strategies for reasoning about programs—in Hoare-style logics,
the concern is mostly invariant discovery—and verify small, but nontrivial, examples.
Such discrete techniques are actively pursued in program verification, or, in the static
analysis community. This paper aims to exemplify our framework’s potential for transferring static analysis techniques to hybrid applications. In it we rely on nonstandard
analysis; hence our venture is called nonstandard static analysis. We have implemented
a prototype that generates a precondition, given a program and a postcondition.
In what follows we present the strategies for simplification and invariant/precondition
discovery that we implemented, and prove their correctness. In fact we only present thestrategies’ standard version—i.e. for W HILE and H OARE, as opposed to the nonstandard version that is for W HILEdt and H OAREdt . This is because the transfer from theformer to the latter is routine work. Soundness of the nonstandard version follows fromthat of the standard one, almost trivially via the sectionwise lemmas. We will demonstrate this process using one of the strategies, in §4.2.
A related issue is the legitimacy of use of Mathematica for symbolic computationin our prototype. What we prove in Mathematica are formulas about real numbers, nothyperreals; and this needs justification. In §5.2 we address this issue and show that
proofs in Mathematica indeed prove formulas about hyperreal numbers. The key is thetransfer principle, a celebrated result in NSA (see §2 later).
We defer most of the proofs to the appendix.
Related work. There have been extensive research efforts towards hybrid systems fromthe formal verification community. Unlike the current work where we turn flow into
jump via dt, most of them feature acute distinction between flow- and jump-dynamics.
Model-checking approaches to hybrid systems have been studied for quite a while,with the successful formalism of hybrid automaton [1], on the one hand. On the other
hand, deductive approaches have seen great advancement through a recent series ofwork by Platzer and his colleagues (including [12, 14]), resulting in the automated3

prover KeYmaera. Our nonstandard static analysis approach currently falls much shortof theirs in scalability and sophistication. However some of their techniques can betranslated into the techniques in our framework; one example is the differential invariant strategy (§5.3). Interestingly in [14] it is argued that: being hybrid imposes no additional burden to verification in principle. This concurs with our claim.
Research in static analysis resulted in a huge number of verification techniques—[4, 7, 18] to name just a few. Some of them have been already used for hybrid applications (modeled with explicit differential equations) [16, 17, 19]. Our thesis is thatthese discrete techniques can be transferred to hybrid applications as they are, via NSA.
In §4.1 we transfer the phase split technique in [20].
The use of NSA as a foundation of hybrid system modeling is not proposed for the
first time; see e.g. [3, 5, 8]. Compared to this existing work, we claim our novelty is theuse of NSA machinery (notably the transfer principle) in actual, automatic verification.
One recent research program (resulting e.g. in [6]) aims to employ continuous
techniques—from the theory of dynamical systems—in purely discrete programs andapplications. This is opposite to our approach (discrete techniques applied to continuous applications). We believe, however, that the two directions are not contending ones.
It is not at all our intention here to champion the superiority of discrete techniques; ourpoint instead is that the collection of available discrete techniques has much wider applicability. It is indeed our future work to combine discrete and continuous techniques.

2 Preliminaries
We summarize our previous work [21], focusing on providing intuitions. We denote thesyntactic equality by ≡.
Nonstandard Analysis. For detailed expositions see e.g. [9, 11].
We fix an ultrafilter F ⊆ P(N) that extends the cofinite filter Fc := {S ⊆ N |N \ S is finite}. Its properties to be noted: 1) for any S ⊆ N, exactly one of S and N \ S
belongs to F; 2) if S is cofinite (i.e. N \ S is finite), then S belongs to F.
Definition 2.1 (Hypernumber d ∈ ∗D) For a set D (typically it is N or R), we define
the set ∗D by ∗D := DN / ∼F . It is the set of infinite sequences on D modulo thefollowing equivalence ∼F : we define (d0 , d1 , . . . ) ∼F (d′0 , d′1 , . . . ) by{i ∈ N | di = d′i } ∈ F ,for which we say “di = d′i for almost every i.”

Therefore, given that two sequences (di )i and (d′i )i coincide except for finitely many
indices i, they represent the same hypernumber. Other predicates (such as <) are definedin the same way. For example a hyperreal ω −1 := [ (1, 12 , 31 , . . . ) ] is positive (0 < ω −1 )but is smaller than any (standard) positive real r = [(r, r, . . . )].
The framework of W HILEdt , A SSNdt and H OAREdt . We take the standard combination (e.g. in [22]) of a while-style programming language W HILE, a first-order assertion
language A SSN and a Hoare-style program logic H OARE (we equip them with constants
for all real numbers). Then we augment the framework with a constant dt that denotes

4

a specific infinitesimal ω −1 = [ (1, 21 , 31 , . . . ) ], and obtain the nonstandard framework
consisting of W HILEdt , A SSNdt and H OAREdt .
Definition 2.2 (W HILEdt , W HILE, A SSNdt , A SSN) The syntax of W HILEdt is:
AExp ∋

a ::= x | r | a1 aop a2 | dt
where x ∈ Var, r is a constant for r ∈ R, and aop ∈ {+, −, ·, /, ⌈ ⌉}BExp ∋

b ::= true | false | b1 ∧ b2 | ¬b | a1 < a2

Cmd ∋c ::= skip | x := a | c1 ; c2 | assert b | if b then c1 else c2 | while b do c

Here AExp is the set of arithmetic expressions; BExp and Cmd are those of Boolean
and command expressions. The operator ⌈r⌉ denotes the smallest natural number whichis larger than or equal to the real number r. We will use this operator in §5.4. The command assert b amounts to skip if b is true; an infinite loop (divergence) otherwise.
Our first-order assertion language3 A SSNdt consists of the following formulas.
Fml ∋ A ::= true | false | A1 ∧ A2 | ¬A | a1 < a2 |∀x ∈ ∗N. A | ∀x ∈ ∗R. A
where x ∈ Var and ai ∈ AExp
By W HILE, we denote the fragment of W HILEdt without the constant dt.
By A SSN we designate the language obtained from A SSNdt by: 1) dropping theconstant dt; and 2) replacing the quantifiers ∀x ∈ ∗N and ∀x ∈ ∗R with ∀x ∈ N and∀x ∈ R, respectively, i.e. with those which range over standard numbers.
It is essential that in A SSNdt we allow only hyperquantifiers ∀x ∈ ∗R and notstandard ones ∀x ∈ R. This is much like with the transfer principle in NSA [11,Thm. II.4.5].
Definition 2.3 (Section e|i ) Let e be an expression of W HILEdt or A SSNdt , and i ∈ N.
The i-th section of e, denoted by e|i , is obtained by: 1) replacing every occurrence ofdt with the constant 1/(i + 1); and 2) replacing every hyperquantifier ∀x ∈ ∗D with∀x ∈ D. Here D ∈ {N, R}. Obviously a section e|i is an expression of W HILE or A SSN.
Definition 2.4 (H OAREdt , H OARE) H OAREdt is a system that derives Hoare triples{A}c{B} (a triple of A SSNdt formulas A, B and a W HILEdt command c) using thefollowing rules. The rules are the same for H OARE.
(A SSIGN )˘¯(S KIP )A[a/x] x := a {A}{A} skip {A}{A} c1 {C} {C} c2 {B}{A ∧ b} c1 {B} {A ∧ ¬b} c2 {B}(S EQ )(I F ){A} c1 ; c2 {B}{A} if b then c1 else c2 {B}′′′′{A ∧ b} c {A}|= A ⇒ A {A } c {B } |= B ⇒ B(W HILE )(C ONSEQ ){A} while b do c {A ∧ ¬b}{A} c {B}{b ⇒ A} assert b {A}(A SSERT )We write ⊢ {A}c{B} if the triple {A}c{B} can be derived using the above rules.
3

The term assertion language has little to do with the command assert b in W HILEdt .

5

We turn to semantics. Denotational semantics of W HILEdt is defined following theintuition in Example 1.1. There the semantics JcK of a command c is a hyperstate transformer that maps a hyperstate σ (a state that stores hypernumbers) to a hyperstate JcKσ.
Semantics of an assertion A ∈ Fml is defined in the usual way; we write |= A andsay A is valid if σ |= A for each hyperstate σ. A Hoare triple is valid (|= {A}c{B})if, for any hyperstate σ such that σ |= A, we have JcKσ |= B.
Three sectionwise lemmas play central roles in our framework. They correspond toŁoś’s theorem in NSA. We only present the following one, that is the most relevant tothe current paper. Recall the meaning of “for almost every i” via an ultrafilter (§2).
Lemma 2.5 (Sectionwise validity of Hoare triples) Let A, B be A SSNdt formulas, andc ∈ Cmd be a W HILEdt command. We have|= {A}c{B}⇐⇒|= A|i c|i B|i for almost every i.
⊓⊔
Definition 2.6 (∗-transform) Let A be an A SSN formula. We define its ∗-transform,
denoted by ∗A, to be the A SSNdt formula obtained from A by replacing every occurrence of a standard quantifier ∀x ∈ D with the corresponding hyperquantifier ∀x ∈ ∗D.

Proposition 2.7 (Transfer principle) 1. For each A SSN formula A, |= A iff |= ∗A.
2. For any dt-free A SSNdt formula A, the following are equivalent: 1) |= A|i for eachi ∈ N; 2) |= A|i for some i ∈ N; 3) |= A.
⊓⊔

3 A Leading Example: ETCS
We use verification of (a simplified version of) the European Train Control System(ETCS) as a leading example—this is done also in many chapters of [13]. We go stepby step, introducing the strategies as the need arises.
Fig. 1. The original program
Our target program ETCS0 is shown on the right. It ETCS
0contains small fragments of the European Train Control
System (ETCS). Here a, t, v, and z are variables that while (v > 0) {if m - z < srepresent acceleration rate, time, velocity, and position,then a := -belse a := a0;
respectively. The symbols m, s, b, a0, eps are all cont := 0;
stants, all of which are assumed to be (strictly) positive.
while (t < eps && v > 0) {z := z + v * dt;
Here, m is the position beyond which the train must notv := v + a * dt;
run (“a wall”); s is the safety distance such that, oncet := t + dt }}the train’s distance from the wall is less than s, it starts (: z < m :)braking; b is the rate used in braking; a0 is the (positive) acceleration rate used unlessthe train is braking. The check if m − z < s occurs once every eps seconds.
The (post)condition to be guaranteed after the execution of ETCS0 is the safety property z < m; it is inserted in Fig. 1 as an annotation, between (: and :). We set out tocalculate a precondition—a relationship among constants as well as (the initial valuesof) the variables—that ensures this postcondition.
The program ETCS0 is itself a while-loop; thus to calculate a precondition we needto discover a (loop) invariant. However the loop is a complicated one with an if branch
and another while-loop inside. We first preprocess ETCS0 and simplify it, employing
some program transformation strategies studied in the field of static analysis.

6

4 Program Simplification Strategies
4.1

Phase Split

Looking at ETCS0 (Fig. 1), we can imagine that once the train starts braking, it neverstarts to accelerate. That is, we could transform the outer loop in ETCS0 into two successive loops, with the former loop solely for accelerating and the latter loop for braking.
It is the program transformation technique proposed while b do . . . (if . . . ) . . .
gin [20] (closely related to those in [2, 10]) that makes
23
the above intuition rigorous. It eliminates an if-branch
6 while bg ∧ ¬bs do . . . ; 7
into 4
5
inside a while loop using a phase splitter predicate bs , aswhile bg ∧ bs do . . .
is shown on the right. This simplification strategy shallbe referred to as phase split.
First we follow [20] and describe the strategy formalized in W HILE and H OARE.
In §4.2 we use the sectionwise lemmas and show that the nonstandard framework(W HILEdt and H OAREdt ), too, admits the same strategy.
Definition 4.1 (Holed command, pre-hole fragment) The set Cmd[ ] of holed commands of W HILE—those which contain exactly one hole [ ] for a guard of if—is defined by the BNF expression below. Here c, c1 , c2 ∈ Cmd are commands (withoutholes). The result of replacing [ ] with b ∈ BExp in h ∈ Cmd[ ] is denoted by h[b].
Cmd[ ] ∋ h ::= if [ ] then c1 else c2 | h; c | c; h |if b then h else c | if b then c else hif [ ] then c1 else c2 :≡ skiph; c :≡ hc; h :≡ c; hif b then h else c :≡ assert b ; hif b then c else h :≡ assert ¬b ; h

For each holed command h, its pre-hole fragment h is defined inductively as above.
Intuitively, it is the fragment of h that is executed before hitting the hole [ ].
Lemma 4.2 (Phase split [20]) If a Boolean expression bs ∈ BExp satisfies|= {bs } h {bc } , |= {¬bs } h {¬bc } , and |= bg ∧ bs h[bc ] ¬bg ∨ bs

, (2)then we have Jc0 K = Jc1 K between the commands
c0
c1

:≡
:≡

while bg do h[bc ] , and
while (bg ∧ ¬bs ) do h[false] ; while (bg ∧ bs ) do h[true] .

(3)
⊓
⊔

Such bs is called a phase splitter predicate. In ap- Fig. 2. The program ETCS1
plying this lemma to ETCS0 , an obvious candidate for awhile (v > 0 && m - z >= s) {phase splitter predicate is m − z < s, the guard of thea := a0;t := 0;while (t < eps && v > 0) {if-branch itself. (Its negation m − z ≥ s is a candidate
z := z + v * dt;
too; but the side conditions (2) cannot be discharged.)v := v + a0 * dt;
t := t + dt }};To discharge the side conditions (2) is not hard: inwhile (v > 0 && m - z < s) {its course we use the differential invariant strategy dea := -b;t := 0;while (t < eps && v > 0) {scribed later in §5.3. We further apply obvious simplifiz := z + v * dt;
cations, such as Jif true then c1 else c2 K = Jc1 K
v := v - b * dt;
t := t + dt }}and constant propagation; consequently we are led to the(: z < m :)program ETCS1 (on the right) that is equivalent to ETCS0 .

7

4.2

From Standard to Nonstandard I: Modular Transfer

As stated in the introduction, the current paper presents strategies (for simplificationand invariant/precondition discovery) only for the standard framework (W HILE andH OARE), leaving out the corresponding nonstandard strategies (for W HILEdt and H OAREdt ).
This is because the transfer from the former to the latter is straightforward. Here we describe the process of such transfer, with the phase split strategy (§4.1) as an example.
Here the sectionwise lemmas (in particular Lem. 2.5) play the key role.
The syntactic notions of holed command and pre-hole fragment are defined in
W HILEdt , in the exactly the same way as in W HILE (Def. 4.1).
Lemma 4.3 (Nonstandard phase split) Assume bs ∈ BExp satisfies, in H OAREdt ,|= {bs } h {bc } , |= {¬bs } h {¬bc } , and |= bg ∧ bs h[bc ] ¬bg ∨ bs .

Let c0 and c1 be as in (3), now in W HILEdt . We have Jc0 K = Jc1 K.

⊓⊔

Proof. Let σ ∈ HSt be a hyperstate; and (σ|i )i∈N be its arbitrary sequence representation. By the definition of hypernumbers, it suffices to show that
Jc0 |i K(σ|i ) = Jc1 |i K(σ|i )for almost every i.

(4)

By the assumptions and Lem. 2.5, each one of the following holds for almost every i.
|= {bs |i } h|i {bc |i } |= {(¬bs )|i } h|i {(¬bc )|i } |= (bg ∧ bs )|i h[bc ]|i (¬bg ∨ bs )|i .
Therefore, by the definition of ultrafilter, all three of the above hold simultaneously, foralmost every i. That is, for almost every i, we have all of the following three hold:|= {bs |i } h|i {bc |i } |= {¬(bs |i )} h|i {¬(bc |i )} |= bg |i ∧ bs |i h|i [bc |i ] ¬(bg |i ) ∨ bs |iwhere we also used an obvious fact h |i ≡ (h|i ). To each such i we apply the standard
version of the strategy (Lem. 4.2) and obtain, for almost every i,qywhile bg |i do h|i [bc |i ] (σ|i )qy= while (bg |i ∧ ¬bs |i ) do h|i [false] ; while (bg |i ∧ bs |i ) do h|i [true] (σ|i )Using another obvious fact that h[bs ] |i ≡ h|i [bs |i ], this is equivalent to (4).
⊓⊔Note the modularity in the proof: the standard version’s proof (Lem. 4.2) is completely
hidden. For any other (standard) strategy presented in this paper, its nonstandard version
follows in the same way via sectionwise arguments.
4.3

Superfluous Guard Elimination

In ETCS1 each while-loop has its guard consisting of two atomic inequalities. This
causes problems with our toolkit for invariant/precondition discovery, especially withthe counting iterations strategy (§5.4). In fact, some of the conditions are seemingly
superfluous: for example, in the second (internal) while-loop, m − z < s is an invariant.

8

Lemma 4.4 (Superfluous guard elimination) For commands
c0
c1

:≡
:≡

while (b ∧ bsf ) do c , and
if bsf then while b do c else skip ,if we have |= {b ∧ bsf } c {bsf }, then Jc0 K = Jc1 K.

⊓⊔

This strategy, together with some straightforward simplifications, transforms ETCS1
into ETCS2 shown below. For each of the three instances of the strategy, the side condition is easily discharged using the differential invariant strategy (§5.3).
The program
ETCS2 :

4.4

if (v > 0)
thenwhile (m - z >= s) {a := a0;t := 0;while (t < eps) {z := z + v * dt;
v := v + a0 * dt;
t := t + dt }}else skip;

while (v > 0) {a := -b;t := 0;while (t < eps && v > 0) {z := z + v * dt;
v := v - b * dt;
t := t + dt }}(: z < m :)Time Elapse

The challenge in verifying W HILE programs is in while-loops. The second half of
ETCS2 is a loop with another loop inside; we wish to simplify this.
A close look reveals that the inside loop is vacuous: since the inside guard and theoutside guard share the same condition v > 0, the condition t < eps has in fact noeffect.4 We often encounter this situation in the verification of W HILEdt programs—
other simplification strategies easily lead to such vacuous nested loops.
Lemma 4.5 (Time elapse) Let t be a variable that does not occur in b ∈ BExp orc ∈ Cmd; ε be a positive constant; andc0 :≡ while b do t := 0; while (t < ε ∧ b) do (t := t + dt; c) ,c1 :≡ while b do c .
Then the denotations Jc0 K and Jc1 K coincide on all variables but t.

⊓⊔

Lem. 4.5 allows several straightforward generalizations. Currently we do not need them.
Since t does not occur in the postcondition z < m, Lem. 4.5 ensures that time elapse
is a sound transformation. It simplifies the second half of ETCS2 into ETCS3 below.
The program
ETCS3 :

4

if (v > 0)
thenwhile (m - z >= s) {a := a0;t := 0;while (t < eps) {z := z + v * dt;
v := v + a0 * dt;
t := t + dt }}else skip;

while (v > 0) {a := -b;z := z + v * dt;
v := v - b * dt }(: z < m :)This is not the case with the first half of ETCS2 : it might be m − z < s but still the train canaccelerate for eps seconds. Therefore the nested loops cannot be suppressed so easily.

95 Precondition/Invariant Discovery Strategies
We now describe three strategies aimed at the discovery of suitable preconditions/invariants
for while-loops. In fact they return directly a precondition (when they succeed).
We desire their output to be quantifier-free, since quantifiers often incur prohibiting
performance penalties. This is what we do in our prototype: quantifiers appear only in
the Mathematica backend. In what follows several quantifiers do occur; but they are in
the correctness proofs of the strategies, i.e. on the meta level.
5.1

Invariant via Quantifier Elimination

We now compute a precondition precond1 that, after the execution of the last whileloop in ETCS3 (which we denote by cbrake ), ensures the postcondition z < m hold.
Recall our thesis: via nonstandard analysis, we can represent continuous flow bydiscrete jumps, so that (discrete) verification techniques readily apply. However, once
we cast a continuous look at cbrake , it obviously represents a simple flow dynamics governed by the differential equations v̇(t) = z̈(t) = −b. In this “continuous” perspective,
one would solve the current question in the following way.
– First the differential equations are solved analytically, obtaining v(t) = v0 − bt andz(t) = z0 + v0 t − 21 bt2 . Here v0 and z0 are initial values.
– Using these analytic solutions, the desired precondition is nothing other than1z0 + v0 t − bt2 < m .
(5)
2
One would then apply quantifier elimination and obtain a quantifier-free formulathat is equivalent to (5). Some algorithms are known including cylindrical algebraic
decomposition (CAD). In Mathematica Resolve offers this functionality; it returns∀t ∈ R.

v0 − bt > 0 ∧ t ≥ 0=⇒v0 ≤ 0 ∨ ( z0 < m ∧ 2bm − v02 − 2bz0 ≥ 0 ) .
This procedure of “first solve differential equations, then eliminate quantifiers” is common in the deductive verification of hybrid systems, such as in Platzer’s [13].
The next strategy (Lem. 5.2) is a discrete variation of this procedure, where differential equations are replaced with difference equations (also called recurrence relations).
y times}|{z
We need preparation. In Lem. 5.2 we need to have a formula A [a/x][a/x] · · · [a/x]as a formula with y as a free variable. This is not automatic—note that substitution[a/x] and the number y live on the meta level. However, let us say that A is a formulaA ≡ (x > 0) and a ≡ x + 1. Then we have, for any y ∈ N,
|=x > 0 [x + 1/x] [x + 1/x] · · · [x + 1/x] ⇔ x + y > 0 ,where substitution is repeated y times. Thus the formula x+y > 0 effectively represents
the formula ( x > 0 ) [x + 1/x] [x + 1/x] · · · [x + 1/x]. In other words, x + y > 0 is ahomogeneous representation of substitutions x > 0, x + 1 > 0, (x + 1) + 1 > 0, . . . .
The general definition is as follows. There Ars corresponds to x + y > 0 in theabove example; it is a formula that must be discovered somehow. In our prototype it isdone by solving a recurrence relation.

10

Definition 5.1 (Repeated substitution) Let x be a variable, A be a A SSN formula, abe an arithmetic expression, and y be a variable not occurring in A, a or x. A formula
Ars is said to be a homogeneous representation of A and [a/x] if the following holds.
|= Ars [0/y] ⇔ A ∧ ∀u ∈ N. Ars [u + 1/y] ⇔ Ars [u/y] [a/x](6)

We abuse notations by denoting such Ars by A[a/x]y .

Lemma 5.2 (QE invariant)(¬b ⇒ A) ∧|=
while b do x := a A
y
y+1
y+1
∀y ∈ N. ( b[a/x] ∧ ¬b[a/x]) ⇒ A[a/x]The lemma is presented in the simplest form: it is straightforward to allow a sequencex1 := a1 ; . . . ; xn := an of assignments inside the loop.

Proof. Let P
be the precondition (¬b ⇒ A) ∧ ∀y ∈ N. b[a/x]y ∧ ¬b[a/x]y+1 ⇒A[a/x]y+1 . By the (W HILE ) rule of H OARE, it suffices to show that: 1) P is a loop
invariant, that is, |= {P ∧ b}x := a{P }; and 2) P is strong enough, i.e. |= P ∧ ¬b ⇒ A.
To prove 1), assume σ |= P ∧ b. The goal is Jx := aKσ |= P , which is equivalent toσ |= P [a/x], since P [a/x] is the weakest precondition for x := a and the postcondition
P . This is further reduced to: σ |= b[a/x]n+1 ∧ ¬b[a/x]n+2 ⇒ A[a/x]n+2 for any
n ∈ N (which follows from σ |= P ); and σ |= ¬b[a/x] ⇒ A[a/x] (which follows fromσ |= b and σ |= ( b ∧ ¬b[a/x] ) ⇒ A[a/x]).
The condition 2) is obvious since |= P ⇒ (¬b ⇒ A). This concludes the proof. ⊓⊔yIn our prototype, we first compute homogeneous representations b[a/x]and A[a/x]yy+1y
by solving recurrence relations in y such as A[a/x]= A[a/x] [a/x]. Using this
we form the precondition in Lem. 5.2. Then we further eliminate the quantifier ∀y ∈ N
and obtain a quantifier-free precondition.
For example, in the case of cbrake in ETCS3 , we discover a homogeneous repre→→
sentation A[−a /−x ]y :≡ 12 (bdt2 y + 2dtvy − bdt2 y 2 + 2z) < m. As a quantifier-free
precondition we obtain the following, which is henceforth denoted by P1 .

`´
P1 :≡ (v > 0 ∨ m > z) ∧ b2 dt2 + 4bdtv + 8bz + 4v 2 < 8bm ∨ bdtv + 2bz + v 2 ≤ 2bm(7)

This strategy (Lem. 5.2) has the merit of having no side conditions. But in our
experience it is computationally expensive: a slightly complicated postcondition (say, acombination of a few inequalities) makes the quantifier elimination step infeasible. Infact it does not currently work for the loops in ETCS3 other than the last one cbrake .
5.2

From Standard to Nonstandard II: The Transfer Principle and Symbolic
Computation in Mathematica

Here again we demonstrate how a standard strategy can be transferred to a nonstandard
one. The strategy QE invariant (Lem. 5.2) employs Mathematica in two stages: solving recurrence relations and eliminating quantifiers, both done over standard numbers(instead of hyperreals). Our focus is therefore on how this can be justified.

.

11

Definition 5.3 (Repeated substitution in A SSNdt ) Let x, A, a, y be as in Def. 5.1, but
now in A SSNdt . A formula A′rs is said to be a homogeneous representation of A and[a/x], and is denoted by A[a/x]y , if the following holds.
|= A′rs [0/y] ⇔ A ∧ ∀u ∈ ∗N. A′rs [u + 1/y] ⇔ A′rs [u/y] [a/x](8)The sole difference from Def. 5.1 is the quantifier (ranging over hypernatural numbers).
How do we find A′rs that satisfies (8)? We rely on the following lemma.

Lemma 5.4 In the setting of Def. 5.3, let A′ and a′ be the expressions obtained from
A and a by replacing the constant dt by a fresh variable d (and also by making hyperquantifiers standard). If Ars is a homogeneous representation A′ [a′ /x]y in A SSN(Def. 5.1), then ∗Ars [dt/d] is a homogeneous representation Ars [a/x]y in A SSNdt . ⊓⊔Therefore it essentially suffices to prove (6). This is in A SSN hence Mathematica iscapable of proving it.
Lemma 5.5 (Nonstandard QE invariant) We have, in H OAREdt ,(¬b ⇒ A) ∧|=
while b do x := a A
∗
y
y+1
y+1
∀y ∈ N. b[a/x] ∧ ¬b[a/x]⇒ A[a/x]
Proof. By Lem. 2.5, the following suffices: in H OARE, (¬b ⇒ A) ∧while b|i do 


A|i
|=
x := a|i∀y ∈ ∗N. b[a/x]y ∧ ¬b[a/x]y+1 ⇒ A[a/x]y+1
iholds for almost every i ∈ N. By Def. 5.3, Def. 5.1 and [21, Lem. 4.5], it is easy that|= A[a/x]y |i ⇔ A|i [a|i /x]y for almost every i ∈ N. Therefore it suffices to show

while b|i do 
A|i
x := a|i

for almost every i. The last statement (in H OARE) is Lem. 5.2 itself.

⊓
⊔

|=

(¬b|i ⇒ A|i ) ∧∀y ∈ N. b|i [a|i /x]y ∧ ¬b|i [a|i /x]y+1 ⇒ A|i [a|i /x]y+1

The second use of Mathematica—in quantifier elimination—is justified much likein Lem. 5.4, via the transfer principle.
5.3

Differential Invariant

Most of the simplification strategies in §4 come with side conditions to be discharged. In
many such cases, the postcondition to be established is itself an invariant. An example
is the condition v > 0 in the first half of ETCS1 .
The following lemma provides an efficient method for proving such Hoare triples.5
5The name is taken from Platzer’s extensive treatment of a similar notion [13]. The correspondence is as follows: when the while-loop below represents continuous dynamics, the condition
ac [a/x] < ac means that the first derivative of ac is negative.

.

12

Lemma 5.6 (Differential Invariant) Assume that an arithmetic expression ac satisfies|= b ⇒ ac [a/x] < ac . Then |= {ac < 0} while b do x := a {ac < 0}.
⊓⊔In our current prototype a candidate for the invariant ac < 0 is chosen simply out of the
disjuncts of the postcondition. More sophisticated candidate generation methods—suchas in [13]—are left as future work.
5.4

Iteration Count

Verification of the leading example ETCS (§3) has been reduced, in §5.1, to the situation
below on the left. Here postcondition P1 is as in (7). Our prototype further simplifies
the situation into the one on the right.
if (v > 0)
thenwhile (m - z >= s) {a := a0;t := 0;while (t < eps) {z := z + v * dt;
v := v + a0 * dt;
t := t + dt }}else skip(: P_1 :)while (m - z >= s) {a := a0;t := 0;while (t < eps) {z := z + v * dt;
v := v + a0 * dt;
t := t + dt }}(: P_2 :)(9)where P2 :≡ b2 dt2 + 4bdtv + 8bz +4v 2 < 8bm ∨ bdtv + 2bz + v 2 ≤ 2bm

We now face a nested loop to which none of the previous strategies applies. Our last
strategy estimates the number of iterations in each loop—such as eps/dt for the inner loop6 —and approximates commands by repeated applications of assignments. The
strategy involves nontrivial side conditions but we experienced its wide applicability.
The formalization of the full iteration count strategy is cumbersome and buries its
idea in overwhelming details. Here we only present the following restricted version that
deals with a single loop. The full version that applies to nested loops is deferred to theappendix.
Lemma 5.7 Let ai be an arithmetic expression. Assume the following conditions.
1. |= ¬b[a/x]aiy
2. For some fresh variable y, |= ¬b[a/x]y+1 c ¬b[a/x]u
3. |= ∀u, v ∈ R. ai ≤ u < v <∧ ¬b[a/x]⇒ ¬b[a/x]v
 ai + 1 y+1y
4. For some fresh variable y, |= A[a/x]c A[a/x]v
u
5. |= ∀u, v ∈ R. u < v ∧ A[a/x] ⇒ A[a/x]Then we have|=A[a/x]ai +1 ∧ ai ≥ 0 while b do c {A} .

(10)
⊓
⊔

Here are some intuitions. The expression ai denotes an estimated number of iterations:for example, ai ≡ eps/dt for the inner loop on the right in (9). The estimation is doneby solving the equation ai · dt = eps. We are also simulating execution of c by a
6

Note that the number eps/dt makes sense in NSA: it means (i + 1) · eps in the i-th section.

13

substitution [a/x]; the conditions 2. and 4. assert that this simulation is sound. Note thatthese conditions are trivially satisfied if c is an assignment command x := a.
The conditions 3. and 5. impose suitable monotonicity requirements on the guardb and the postcondition A. Such monotonicity is needed for the following reason. The
estimated number ai of iterations need not be exactly some (hyper)natural number—it
can lie between two (hyper)natural numbers, i.e. ⌈ai ⌉ − 1 < ai < ⌈ai ⌉. This is why
we are conservative in (10); we use ai + 1, instead of ai , as a number of iterations. The
monotonicity conditions (3. & 5.) ensure that this conservative approximation is sound.
The full version of this iteration count strategy (Lem. 5.7) succeeds in the remaining bit of the leading example (on the right in (9)). Its output is a Boolean combinationof inequalities; we denote this formula by P3 . It is complicated—not least due to occurrences of dt—and we would rather not write it down explicitly.
5.5

Cast to Shadow

We have established that |= {P3 } ETCS0 {z < m}. As the last step, we wish toeliminate the occurrences of dt in the precondition P3 . This results in a much simpler
precondition. The intuition is: the condition ε + dt < 0 is implied by ε < 0 if ε is aconstant denoting a standard real number. To put it in rigorous terms:
Lemma 5.8 (Cast to Shadow) Let a be an arithmetic expression in W HILEdt , d be a
fresh variable, and a[d/dt] be the expression in W HILE obtained by substituting d for
dt in a. Assume the following.
1. The expression a is closed, that is, it has no occurrences of variables.
7
2. Let σ be a (standard) state that
 is not ⊥; it determines a function fσ : R → R
by r 7→ Ja[d/dt]K σ[d 7→ r] . We assume that fσ is continuous at r = 0 for any
given σ 6= ⊥. Here Ja[d/dt]K is defined by denotational semantics [21, §3.2]; andσ[d 7→ r] is an updated state.
Then |= a[d/dt] [0/d] < 0 =⇒ a < 0.
⊓⊔
Note that, by the definition of a[d/dt], the expression a[d/dt] [0/d] is the resultof replacing dt in a with 0—i.e. of “eliminating dt.” In using the lemma, the closedness assumption (Cond. 1.) can be enforced by setting the initial values of variables asconstants (that necessarily represent standard reals by the definition of W HILEdt ). The
continuity assumption (Cond. 2.) in the lemma is most of the time satisfied since thearithmetic operations of W HILE are all continuous except for zero-division.
In nonstandard analysis, a hyperreal number r′ that is not infinite has a unique (standard) real number r that is infinitesimally close to r′ (we write r ≃ r′ ). Such r is called
the shadow of r′ ; hence the name of the strategy.
This strategy can be used for simplifying the precondition P3 (or, more generally, a
Boolean combination of inequalities) in the following way.
V W
– First, P3 is converted to CNF (or DNF; it does not matter): |= P3 ⇔ i j Li,j .
Note that every literal Li,j occurs positively.
7

In general a partial function since zero-division might occur.

14– Among all the literals Li,j , the negative ones (like Li,j ≡ ¬(ai,j < bi,j )) is turned
into a positive one (like ai,j ≥ bi,j ), by reversing inequalities.
– Each inequality is turned into the form of either ci,j < 0 or ci,j ≤ 0. For example:Wwe turn ai,j ≥ bi,j into bi,j − ai,j ≤ 0. Thus we have obtained |= P3 ⇔
V
or W
≤.
i
j ci,j ⊳i,j 0 , where each ⊳i,j is either <V– Obviously |= ci,j < 0 ⇒ ci,j ⊳i,j 0; thus |= i j ci,j < 0 ⇒ P3 .
– Finally, to each inequality ci,j < 0 we apply that the side condiV WLem. 5.8 (given
tions are discharged). This establishes |= i j ci,j [d/dt] [0/d] < 0 ⇒ P3 ; thus
we obtain a “simplified” precondition that has no occurrences of dt.
V W
We note that thus obtained precondition i j ci,j [d/dt] [0/d] < 0 is not necessarilyequivalent to P3 , but is stronger (i.e. less general). In our experience, however, the lost
generality is most of the time marginal.
After all, the following is the (core part of the long and extensive) outcome of our
prototype when it is fed with ETCS0 .
` q´
a0 2ε 2a0 (m − s − z0 ) + v02 + bǫ2 + 2m − 2s − 2z0q+ 2bε 2a0 (m − s − z0 ) + v02 + a20 ǫ2 + v02 < 2bs

Here v0 and z0 are constants that designate the initial values of v and z, respectively.

6 Implementation and Experiments
Our prototype implementation takes a W HILEdt program and a postcondition as its input, and tries to calculate a precondition. The tool consists of the following components.
– A native verification condition generator implemented in OCaml. It combines thestandard verification condition generation for Hoare-type logics (such as in [22])and the previously described strategies. It relies on the Mathematica backend formost of the strategies as well as for (symbolic) arithmetic proofs.
– A Mathematica backend that provides functions for the strategies in §4–5. It also
implements some proof strategies for arithmetic formulas.
– A Perl script that serves as an interface between the above two.
Our prototype employs the standard backward reasoning for Hoare-type logics.
When it encounters a while loop, it tries the precondition discovery strategies in §5.
If one or more of those strategies succeed and produce preconditions P1 , . . . , Pn , thenour prototype continues with the disjunction P1 ∨· · ·∨Pn of those preconditions. If not,our prototype tries simplification strategies in §4; the order is phase split, superfluous
guard elimination and then time elapse. If the simplification succeeds, it again tries theprecondition discovery strategies. If not, our prototype reports failure.
Although we sometimes use numeric computations for finding counterexamples, theproofs are established in purely symbolic means. This is a crucial fact for the correctness
guarantee via the transfer principle.
We have tested our prototype against the following W HILEdt programs:– etcs.while: the ETCS example used throughout the paper, and15– zeno.while: the behavior of a bouncing ball.
We conducted both experiments on Fujitsu HX600 with Quad Core AMD Opteron
2.3GHz CPU and 32GB memory. We used Mathematica 7.0 for Linux x86 (64-bit).8
The current implementation is premature. The goals of the experiments have been:
1) the feasibility test of our methodology of nonstandard static analysis, and 2) to drive
theoretical development of static analysis strategies suited for hybrid applications. Enhancing scalability and efficiency of the prototype is left as future work.
etcs.while. Our prototype completed precondition generation for etcs.while in
40.96 seconds (31.97 seconds in the user process and 8.99 in the kernel process), generating the precondition described in §5.5 as an outcome.
zeno.while. We have modeled the behavior of a bouncing ball in W HILEdt and run
our prototype on the program. This program includes the following three parameters:– t0 : ending time of the system;– b: elastic coefficient between the ground and the ball;– h0 : safety height—the ball should not reach higher than this height.
The postcondition is that the peak height of the last bounce is not higher than h0 .
Although the current prototype does not fully succeed to compute a precondition,
it manages to simplify the program substantially. For example, the ascending and descending phases in the movement of the ball are discovered automatically, using Lem. 4.2.
With a manual insertion of one condition (an inequality), our prototype runs throughand outputs a symbolic precondition (which is too long to present here).
Though this bouncing ball example was not fully-automatic, we still find its resultinteresting and encouraging. The example exhibits the Zeno behavior, a big challenge
for many verification techniques (see e.g. [13, Section 3.3.3]). We expect our framework
to be useful in Zeno-type examples, since: 1) it does not distinguish flow dynamics fromjump dynamics (dynamics is always “discrete,” or “all flow dynamics is Zeno”); and 2)
we do not have a governing notion of time (t is a variable just like others).
Discussion. Efficiency or speed of verification is currently not our primary concern;still we noticed several methods for speeding up. For example, calls to the four precondition discovery strategies could be parallelized. Another performance drawback of thecurrent prototype is that the OCaml program and Mathematica communicate via a filewritten to storage, which takes time. A tighter connection via the script mode usage ofMathematica, or Mathlink, is currently looked at.
Acknowledgments Thanks are due to all the reviewers for their careful reading anduseful comments; particularly to the reviewer who pointed out an error in Lem. 5.8.
I.H. is supported by Grants-in-Aid for Young Scientists (A) No. 24680001, JSPS, andby Aihara Innovative Mathematical Modelling Project, FIRST Program, JSPS/CSTP;
K.S. is supported by Grants-in-Aid for JSPS Fellows 23·571.
8The source code of our precondition generator and the input W HILEdt programs are available
at http://www-mmm.is.s.u-tokyo.ac.jp/∼ichiro/papers/vcgen.tgz.

16

References
1. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero,
A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comp. Sci.
138(1), 3–34 (1995)
2. Balakrishnan, G., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Refining the control structureof loops using static analysis. In: EMSOFT. pp. 49–58 (2009)
3. Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybrid systems modelers. J. Comput. Syst. Sci. 78(3), 877–910 (2012)
4. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Ferrante, J.,
McKinley, K.S. (eds.) PLDI. pp. 300–309. ACM (2007)
5. Bliudze, S., Krob, D.: Modelling of complex systems: Systems as dataflow machines. Fundam. Inform. 91(2), 251–274 (2009)
6. Chaudhuri, S., Gulwani, S., Lublinerman, R., NavidPour, S.: Proving programs robust. In:
Gyimóthy, T., Zeller, A. (eds.) SIGSOFT FSE. pp. 102–112. ACM (2011)
7. Colón, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear
constraint solving. In: Jr., W.A.H., Somenzi, F. (eds.) CAV. Lect. Notes Comp. Sci., vol.
2725, pp. 420–432. Springer (2003)
8. Gamboa, R.A., Kaufmann, M.: Nonstandard analysis in ACL2. J. Autom. Reason. 27(4),323–351 (Nov 2001)
9. Goldblatt, R.: Lectures on the Hyperreals: An Introduction to Nonstandard Analysis.
Springer-Verlag (1998)
10. Gopan, D., Reps, T.W.: Guided static analysis. In: Nielson, H.R., Filé, G. (eds.) SAS. Lect.
Notes Comp. Sci., vol. 4634, pp. 349–365. Springer (2007)
11. Hurd, A.E., Loeb, P.A.: An Introduction to Nonstandard Real Analysis. Academic Press(1985)
12. Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log.
Comput. 20(1), 309–352 (2010)
13. Platzer, A.: Logical Analysis of Hybrid Systems—Proving Theorems for Complex Dynamics. Springer (2010)
14. Platzer, A.: The complete proof theory of hybrid systems. Tech. Rep. CMU–CS–11–144,
Carnegie-Mellon Univ., Pittsburgh PA 15213 (2011)
15. Robinson, A.: Non-standard analysis. Princeton Univ. Press (1996)
16. Rodrı́guez-Carbonell, E., Tiwari, A.: Generating polynomial invariants for hybrid systems.
In: Morari, M., Thiele, L. (eds.) HSCC. Lect. Notes Comp. Sci., vol. 3414, pp. 590–605.
Springer (2005)
17. Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed
points. In: Johansson, K.H., Yi, W. (eds.) HSCC. pp. 221–230. ACM (2010)18. Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation usinggröbner bases. In: Jones, N.D., Leroy, X. (eds.) POPL. pp. 318–329. ACM (2004)
19. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems.
Formal Meth. in Sys. Design 32(1), 25–55 (2008)
20. Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. Lect. Notes Comp. Sci., vol.
6806, pp. 703–719. Springer (2011)
21. Suenaga, K., Hasuo, I.: Programming with infinitesimals: A while-language for hybrid system modeling. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP (2). Lect. Notes Comp.
Sci., vol. 6756, pp. 392–403. Springer (2011)
22. Winskel, G.: The Formal Semantics of Programming Languages. MIT Press (1993)

17

A Appendix
A.1 Proofs
Proof of Lem. 2.5 The proof is much like parts of the proofs in [21]. In particular, the‘only if’ part can be proved much like in [21, Lem. 4.5]. The proof is presented anyway
for completeness.
For the ‘if’ part: assume a hyperstate σ satisfies A; and let (σ|i )i∈N be an arbitrary
sequence representation. By [21, Lem. 4.5], we have σ|i |= A|i for almost every i.
It follows from the assumption that Jc|i K(σ|i ) |= B|i . By [21, Lem. 3.10 & 4.5] thisyields JcKσ |= B.
For the ‘only if’ part: assume the negation of the right-hand side. By the definitionof ultrafilter, this means:for almost every i,
6|= A|i c|i B|iwhich in turn is equivalent to:for almost every i, there exists σi ∈ St such that σi |= A|i and Jc|i Kσi 6|= B|i .
Pick such σi ∈ St
such i; for other i’s let σi be, say, ⊥. Then let σ be the for eachhyperstate σ := (σi )i . This hyperstate σ satisfies σ |= A and JcKσ 6|= B, by [21,Lem. 3.10 & 4.5]. This contradicts the assumption that |= {A}c{B}.
⊓⊔
Proof of Lem. 4.2 We follow [20] and prove the lemma using the following sublemma.9qySublemma
A.1
Assume
a
state
σ
∈
St
is
such
that
JhKσ
|=
b
.
Then
h[b
]
σ =
c
c
q
y
h[true] σ.
Proof. By induction on the construction of h ∈ Cmd[ ] .
When h ≡ if [ ] then c1 else c2 : we have h ≡ skip; hence by the assumption,σ |= bc . Thereforeqyh[bc ] σ = Jif bc then c1 else c2 Kσ= Jc1 Kσqy
= Jif [true] then c1 else c2 Kσ = h[true] σ .

by σ |= bc

When h ≡ h′ ; c,qsince yh ≡ hq′ we havey Jh′ Kσ |= bc . Therefore by the induction
hypothesis, we have h′ [bc ] σ = h′ [true] σ. This is used in (∗) below.

9

q
y
q
y
q
y  (∗)qy  qyh[bc ] σ = h′ [bc ]; c σ = JcK h′ [bc ] σ = JcK h′ [true] σ = h[true] σ .

The statement here looks different from that of the original lemma [20, Lem. 1]. The latterholds only if the assertion language is sufficiently expressive; the statement here holds regardless.

18′′
When h ≡ c : h′ , since h ≡ c; h′ we have Jc; hq Kσ |=
y bc , that is,qJh K(JcKσ)y |= bc .
Therefore by the induction hypothesis, we have h[bc ] (JcKσ) = h[true] (JcKσ).
This is used in (∗) below.

q
y
q
y
y
q
y
(∗) q
h[bc ] σ = h′ [bc ] (JcKσ) = h′ [true] (JcKσ) = h[true] σ .
When h ≡ if b then h′ else c, the pre-hole fragment h is h ≡ assert b; h′ .
Therefore the assumption JhKσ |= bc is equivalent to:σ 6|= bor

Jh′ Kσ |= bc .

Now assume σ 6|= b. Thenqyqyh[bc ] σ = if b then h′ [bc ] else c σ= JcKσqy= if b then h′ [true] else c σqy= h[true] σ .

(11)by σ 6|= bqy′ Kσ |= b ; by the induction hypothesis this yields h′ [b ] σ =Otherwise,
by
(11)
we
have
Jh
c
c
q ′
y
h [true] σ. This is used in (∗) below.
qyqyh[bc ] σ = if b then h′ [bc ] else c σqy= h′ [bc ] σ
by σ |= by(∗) q ′= h [true] σqy= if b then h′ [true] else c σqy= h[true] σ .
The other case when h ≡ if b then c else h′ is similar. This concludes the proof.
⊓⊔
Proof. (Of Lem. 4.2) Let us say that a sequence of states σ0 , σ1 , . . . , σk is an execution
trace of c0 if:– Jbg Kσi =q tt foryeach i ∈ [0, k) and Jbg Kσk = ff;– σi+1 = h[bc ] σi for each i ∈ [0, k); and– σi 6= ⊥ for each i ∈ [0, k].
By the definition of denotational semantics, it is obvious that Jc0 Kσ 6= ⊥ if and only if
an execution trace of c0 with σ = σ0 exists; moreover, if that is the case, Jc0 Kσ = σk .
Similarly, we define an execution trace of c1 to be a sequence of states σ0 , σ1 , . . . , σksuch that: there exists l ∈ [0, k] and– Jbg ∧ ¬bKσi = tt for each i ∈ [0, l) and Jbg ∧ ¬bKσl = ff;– Jbg ∧ bKσ
qi = tt foryeach i ∈ [l, k) and Jbg ∧ bKσk = ff;– σi+1 = h[false] σi for each i ∈ [0, l);

19

q
y
– σi+1 = h[true] σi for each i ∈ [l, k); and– σi 6= ⊥ for each i ∈ [0, k].
The number l designates how many times the body of the first loop in c1 is executed. It
is again obvious that: Jc1 Kσ 6= ⊥ if and only if an execution trace with σ = σ0 exists;
and that if that is the case Jc1 Kσ = σk .
It suffices to prove that the above two notions of execution trace (of c0 and of c1 )coincide. The latter is an easy consequence of the following three properties, which are
to be proved.
1. In an execution trace of c0 we have:σi |= b

implies

σi+1 |= b ,for each i ∈ [0, k − 1).

2. In an execution trace of c0 or c1 we have:σi |= b

impliesqyqyh[bc ] σi = h[true] σi ,for each i ∈ [0, k).

3. In an execution trace of c0 or c1 we have:σi 6|= b

impliesqyqyh[bc ] σi = h[false] σi ,for each i ∈ [0, k).

To prove the property 1., assume σi |= bg with i ∈ [0, k − 1). By the definition of
execution
trace ofc0 we have σi |= b; therefore σi |= bg ∧ b. By the assumption that|= bg ∧ b h[bc ] ¬bg ∨ b this impliesqyh[bc ] σi |= ¬bg ∨ b ,that is, σi+1 |= ¬bg ∨ b .

Now, since i + 1 ∈ [0, k), by the definition of execution trace we have σi+1 |= bg ;therefore σi+1 |= b.
To prove the property 2.,
thatq by they assumptionqy |= {b} h {bc } we have JhKσi |= bc ;thus by Lem. A.1 we have h[bc ] σi = h[true] σi . The property 3. is similar.
⊓⊔

Proof of Lem. 4.5 The lemma follows immediately from the following facts, which
are easily proved, and the definition of denotational semantics for while-loops. First,
for any command c, if a variable t does not occur in c thenJcK(σ[t 7→ r]) = (JcKσ)[t 7→ r] ,for any state σ and any real number r ∈ R. Second, if a Boolean expression b ∈ BExp
has no occurrence of t,
JbK(σ[t 7→ r]) = JbKσ ,for any state σ and any real number r ∈ R.

20

Proof of Lem. 5.4 Ars = A′ [a′ /x]y means that the following holds. Note the formulais dt-free.
|= Ars [0/y] ⇔ A′ ∧ ∀u ∈ N. Ars [u + 1/y] ⇔ Ars [u/y] [a′ /x](12)

From this the following is trivial.


Ars [0/y] ⇔ A′ ∧ ∀u ∈ N. Ars [u + 1/y] ⇔ Ars [u/y] [a′ /x](13)
Here we appeal to the transfer principle (Prop. 2.7) and obtain, in A SSNdt ,|= ∀d ∈ ∗R. ∗Ars [0/y] ⇔ ∗A′ ∧ ∀u ∈ ∗N. ∗Ars [u + 1/y] ⇔ ∗Ars [u/y] [a′ /x].
(14)
Now that we are in A SSNdt , we take the instance of (14) with d = dt and obtain|= (∗Ars [dt/d])[0/y] ⇔ A ∧
(15)


∀u ∈ ∗N. (∗Ars [dt/d])[u + 1/y] ⇔ (∗Ars [dt/d])[u/y] [a/x],|= ∀d ∈ R.

where we used obvious syntactic equalities ∗A′ [dt/d] ≡ A and a′ [dt/d] ≡ a. The condition (15) means that ∗Ars [dt/d] is indeed a homogeneous representation (Def. 5.3).
⊓⊔
Proof of Lem. 5.6 It suffices to show |= {ac < 0 ∧ b} x := a {ac < 0}; this follows
immediately from the side condition.
⊓⊔
Proof of Lem. 5.7 We claim that the following formula P
P :≡ ∃z ∈ N. Q
where

Q :≡ ∀u ∈ N. u < z ⇒ b[a/x]u ∧ ¬b[a/x]z ∧ A[a/x]z

is a loop invariant.
Firstly we prove that P is indeed a loop invariant. Assume σ |= b ∧ P . Then there
exists a natural number nlc ∈ N such that σ |= Q[nlc /z]. If nlc = 0 then σ |= b ∧ ¬b;this forces σ = ⊤ and hence trivially JcKσ |= P .
Now assume nlc > 0; we aim at showing JcKσ |= P . By σ |= ¬b[a/x]nlc , nlc > 0
and Cond. 2, we have JcKσ |= ¬b[a/x]nlc −1 . This means there exists at least one natural
number n ∈ N such that JcKσ |= ¬b[a/x]n ; take the smallest such and denote it by′n′lc . Obviously n′lc ≤ nlc − 1; by Cond. 5 we have σ |= A[a/x]nlc +1 ; this further′′
yields JcKσ |= A[a/x]nlc by Cond. 4. By the minimalness requirement on nlc we′ have′u
JcKσ |= ∀u ∈ N. u < nlc ⇒ b[a/x] . Now we have shown JcKσ |= Q[nlc /z],
therefore JcKσ |= P .
Secondly we prove that the precondition P ′ :≡ A[a/x]ai +1 ∧ ai ≥ 0 in (10)′′subsumes P . Assume σ |= P ′ . By Cond. 1 and 3 we have σ |= ¬b[a/x]nlc , where
n′′lc := ⌈Jai Kσ⌉ is the smallest natural number that is larger than or equal to the nonnegative real number Jai Kσ. Therefore at least for one n ∈ N we have σ |= ¬b[a/x]n ;′′′′′take the smallest such and denote it by n′′′lc . Obviously nlc ≤ nlc = ⌈Jai Kσ⌉. Then by′n′′′σ |= P and Cond. 5 we have σ |= A[a/x] lc and this implies σ |= Q[n′′′lc /z], henceσ |= P .
Lastly we have to show |= P ∧ ¬b ⇒ A, which is obvious.
⊓
⊔

21

Proof of Lem. 5.8 It is well-known that the following are equivalent (see e.g. [9,Cor. 7.1.2]): 1) a function f is continuous at c ∈ R; 2) f (x) ≃ f (c) whenever x ≃ c.
Here ≃ means that the two hyperreal numbers are infinitely (or infinitesimally) close
to each other; and the function f in 2) is to be precise the *-transfer ∗f of the originalfunction [9, §3.11]. We have, for each hyperstate σ 6= ⊥,(∗)
JaKσ = Ja[d/dt]K(σ[d 7→ dt]) ≃ Ja[d/dt]K(σ[d 7→ 0]) = J a[d/dt] [0/d]Kσ ,(16)
where (∗) holds from the continuity
assumption(Cond.
2.)
and
that
dt
≃
0.


The expression a[d/dt] [0/d] is dt-free; thus by Cond. 1., the value J a[d/dt] [0/d]Kσ
is in fact a standard real number. It is straightforward that, given a standard real numberr and a hyperreal number r′ such that r ≃ r′ , we have r < 0 imply r′ < 0. Thus (16)yields the claim.
⊓⊔
A.2 The Full Iteration Count Strategy
Lemma A.2 ((Full) iteration count) Let aii and aio be arithmetic expressions. Assume
the following conditions.
`´a1. |= bo [f /y]aii [e/x] io``´v
2. |= ∀u, u′ , v, v ′ , w, w′ ∈ R. 0 ≤ u′ < u∧0 ≤ v ′ < v∧0 ≤ w′ < w∧A [f /y]u [e/x] [f /y]w ⇒
′
`
´
´
′
′
v
A [f /y]u [e/x] [f /y]w
`
´u
`
′
′´
′
′
3. |= ∀u, u , v, v ∈ R. 0 ≤ u < u′ ∧0 ≤ v < v ′ ∧¬bo [f /y]v [e/x] ⇒ ¬bo ([f /y]v [e/x])uaii
4. |= ¬bi [f /y]
5. |= ∀u, v ∈ R. (u < v ∧ ¬bi [f /y]u ⇒ ¬bi [f /y]v )6. |= ∀u ∈ R. (0 ≤ u < aii ⇒ bi [f /y]u )Then we havenoaio +1
A [f /y]aii +1 [e/x]∧ aii ≥ 0 ∧ aio ≥ 0 c0 {A} ,
where

c0

:≡

while bo do

x := e;while bi do y := f



.

(17)

u
Here expressions like A [f /y]v [e/x] are the obvious generalization of Def. 5.1.
In the proof we will use two lemmas: one is Lem. 5.7 and the other is Sublem. A.3
below. Each of them is about estimating the number of iterations for a single loop.
The operator ⌈ ⌉ occurs in the proofs. We note that its use is confined to thebackend and it does not occur in Lem. A.2. Therefore in the actual verification using
Lem. A.2, we do not have to deal with the discontinuous (hence inconvenient) function⌈ ⌉.
Sublemma A.3 Let ai be an arithmetic expression. Assume the following conditions.
1. |= ¬b[a/x]aiai)2. |= ∀u ∈ N. (0 ≤ u < ai ⇒ b[a/x]y
3. For some fresh variable y, |= b[a/x]y+1 c b[a/x]y+1
4. For some fresh variable y, |= ¬b[a/x]c ¬b[a/x]y
5. |= ∀u, v ∈ R. (ai ≤ u < v < ai + 1 ∧ ¬b[a/x]u ⇒ ¬b[a/x]v )

22



6. For some fresh variable y, |= A[a/x]y+1 c A[a/x]yThen we have|=A[a/x]⌈ai ⌉ ∧ ai ≥ 0 while b do c {A} .

(18)

Proof. The proof goes much like the one for Lem. 5.7, with the same invariant P .
Cond. 1–4 forces ai to be a good estimate of the number of iterations; in fact we canprove the latter to be precisely ⌈ai ⌉.
⊓⊔Proof. (Of Lem. A.2) It suffices to prove|=|=aio +1
aio +1
A [f /y]aii +1 [e/x]⇒ A [f /y]⌈aii ⌉ [e/x]
and
n
o

a
+1
io
A [f /y]⌈aii ⌉ [e/x]∧ aii ≥ 0 ∧ aio ≥ 0 c0 {A} .

(19)
(20)

Cond. 2 immediately yields (19). The remaining subgoal (20) is proved using Lem. 5.7;
its side conditions are new proof obligations. Among them, the following two do notfollow immediately from the assumptions of Lem. A.2:ony+1
∧ aii ≥ 0 x := e; while bi do y := f|=
A [f /y]⌈aii ⌉ [e/x]
(21)

y
A [f /y]⌈aii ⌉ [e/x]
,
n
o
y+1
|=
¬bo [f /y]⌈aii ⌉ [e/x]∧ aii ≥ 0 x := e; while bi do y := f
(22)

y
¬bo [f /y]⌈aii ⌉ [e/x].
The obligation (21) is discharged via Lem. 5.7; the obligation (22) is via Lem. A.3.

⊓⊔