Pest Formal Specification
Guido de Caso Diego Garbervetsky Daniel Gorn
Departamento de Computacin, FCEyN, Universidad de Buenos Aires
{gdecaso, diegog, dgorin}@dc.uba.ar
October 9, 2008
1 Introduction
This is the Pest programming language formal specification version 1.0. Pest is an multiprocedural, imperative,
while-style programming language that includes annotations as part of its native syntax.
2 Syntax
We use  to express types (e.g., integers, arrays) and as a typing function that assigns one unique type to each
variable in scope. The set Exp contains the expressions with type  using variables according to .
As basic types, Pest requires the presence of integers and booleans as they are used in annotations and
guards. Note that boolean expressions may quantification, provided it is always bounded (i.e., decidable in
run-time)1. All expressions may also refer to v@pre, the value of the variable v at the beginning of the current
procedure.
We use Sentence;; as the set of every possible sentence that starts with as a typing function and ends
with 0, potentially calling procedures defined in program . A sentence may not change the typing of any
existing variable, but it may extend the typing functions with new variables that appear in the program.
The Pest sentences are defined according to the rules in Figure 1.
(v) =  e 2 Exp
v e 2 Sentence;;
(ASSIGN)
v =2 dom() e 2 Exp
local v e 2 Sentence;;fv 7!g
(DEF)
skip 2 Sentence;;
(SKIP)
s1 2 Sentence;;0 s2 2 Sentence0;;00
s1 s2 2 Sentence;;00
(SEQ)
g 2 ExpBool g is quantifier free
s1 2 Sentence;;0 s2 2 Sentence;;00
if g then s1 else s2 fi 2 Sentence;;
(IF)
g 2 ExpBool g is quantifier free
inv 2 ExpBool var 2 Exp
Int
s 2 Sentence;;0
while g :?! inv :# var do s od 2 Sentence;;
(WHILE)
proc 2 
i 6= j ) cpi 6= cpj pars(proc) = p1; : : : ; pk
(cpi) = proc(pi)
call proc(cp1; : : : ; cpk) 2 Sentence;;
(CALL)
Figure 1: Pest syntax
Pest programs are defined either as empty or by extending an existing program with a new procedure that
potentially calls procedures in that program. Formally, the program set Prog is the smallest set that satisfies:
; 2 Prog
(PROG-EMPTY)
1Note that this does not affect the fact that statically resolving the truth value of a boolean expression is undecidable.
1

 2 Prog proc =2 
dom(proc) = fp1; : : : ; pkg i 6= j ) pi 6= pj
pre; post 2 BoolExpproc
s 2 Sentenceproc; ; 0
; proc(p1; : : : ; pk) :? pre :! post f s g 2 Prog
(PROG-EXTEND)
We define the local variables of a given sentence s as the set of variables that are incorporated by s, formally:
locals(s) = dom(0)r dom()
Note that both procedures and cycles are augmented with annotations such as preconditions, invariants,
variants and postconditions. The following sections make use of these in order to establish a safe notion of
sentence semantics.
3 Operational semantics
A valuation  is a function that maps each variable to a concrete value in its type domain. Valuations can be
updated to reflect that the new value for an already defined variable v is n (noted fv 7! ng), extended to
incorporate a new variable v with an initial value n (noted fnew v 7! ng) or cropped to forget the value of a
set of variables V (noted  V ).
Valuations can be extended to assign values to expressions if the according rules for each expression type are
provided. We will denote JeK = n to say that the valuation  can assign value n to the expression e. Note that
this is not always possible, for instance e may refer to a variable for which  has no associated value.
Finally, the operational semantics of a Pest sentence s that starts from the valuation  and finishes correctly
rendering a valuation 0 is noted  . s . 0. The Pest language operational semantics is defined according to
the rules in Figure 2.
JeK = n
 . v e . fv 7! ng
(O-ASSIGN)
JgK = true  . s1 . 0
 . if g then s1 else s2 fi . 0 locals(s1)
(O-IF-T)
JeK = n
 . local v e . fnew  7! ng (O-DEF)
JgK = false  . s2 . 0
 . if g then s1 else s2 fi . 0 locals(s2)
(O-IF-F)
 . skip .  (O-SKIP)
JgK = false JinvK = true
 . while g :?! inv :# var do s od .  (O-WHILE-F)
 . s1 . 0 0 . s2 . 00
 . s1 s2 . 00
(O-SEQ)
JgK = true JinvK = true JvarK > 0
 . s . 0
JvarK0 < JvarK
0 locals(s) . while g :?! inv :# var do s od . 00
 . while g :?! inv :# var do s od . 00
(O-WHILE-T)
Jpre(proc)K = true  . body(proc) . 0 Jpost(proc)K0 = true
 . call proc(cp1; : : : ; cpk) . fcp1 7! (p1); : : :g
(O-CALL)
(pi)
def
= (cpi)
(pi@pre)
def
= (cpi)
Figure 2: Pest operational semantics
Note that sentence semantics may lock if something goes wrong. For instance, if a loop is cycling and at a
given moment the variant function does not decrease, then the semantics is not defined. The same happens if a
called procedure precondition does not hold in the current valuation, a loop invariant is broken, etc.
4 Static semantics
In order to define static semantics we will first introduce the concept of safe expression condition. Given an
expression e of type , safe(e) is a boolean expression guaranteeing that every valuation  that makes it true can
provide a value for e. For instance, safe(4=y) = y 6= 0.
2

p j= safe(e) 9 v0 (pbv 7! v0c ^ v = ebv 7! v0c) j= q
fpg v e fqg
(S-ASSIGN)
p j= safe(e) p ^ v = e j= q
fpg local v e fqg (S-DEF)
p j= q
fpg skip fqg (S-SKIP)
fpg s1 frg frg s2 fqg
fpg s1 s2 fqg
(S-SEQ)
true j= safe(inv) inv j= safe(g) inv j= safe(var)
p j= inv inv ^ g j= p0 p0 j= var > 0
fp0g var0 var s fq0g
q0 j= inv q0 j= var < var0 inv ^ :g j= q
fpg while g :?! inv :# var do s od fqg (S-WHILE)
p j= safe(g)
p ^ g j= p1 fp1g s1 fq1g q1 j= q
p ^ :g j= p2 fp2g s2 fq2g q2 j= q
fpg if g then s1 else s2 fi fqg
(S-IF)
1  i  k pbcpi 7! pic j= pre(proc)
9o1; : : : ; ok (pbcpi 7! oic ^ post(proc)bpi 7! cpi; pi@pre 7! oic) j= q
fpg call proc(cp1; : : : ; cpk) fqg
(S-CALL)
Figure 3: Pest static semantics
We will use b1 j= b2 to indicate that the boolean expression b1 is stronger than the boolean expression b2.
That is, whenever a valuation makes b1 true, then it makes b2 true as well. Notice that in presence of unbounded
quantification this is an undecidable problem.
Sustitution will be noted e1be2 7! e3c, meaning the expression that results from changing in e1 each occurrence
of e2, putting e3 instead. Notice that e2 and e3 must be of the same type.
We now define the static semantics for a Pest sentence. Instead of operational semantics that act in terms
of valuation updates, static semantics acts by modifying boolean expressions that model many valuations. If p is
a boolean expression that describes the possible valuations before the sentence s, and q is a boolean expression
that describes the possible valuations after s, then fpg s fqg will be the static semantics of s.
The Pest language static semantics is defined according to the rules in Figure 3.
5 Safe programs
There is a clear correlation between Pest’s operational and static semantics. Using the latter, we can give a
notion of safe program. In what follows, if  is a program and p a procedure, then ; p is the program obtained
by appending p to .
Definition 1 (Safe programs). The set Safe of programs is inductively defined as follows:
; 2 Safe
(SAFE-EMPTY)
 2 Safe fpre(p)g body(p) fpost(p)g
; p 2 Safe
(SAFE-EXTEND)
Safe programs are the ones that respect their annotations on any run. That is, for each procedure whenever
the precondition holds then the execution flows normally, satisfying every called procedure precondition and loop
invariants, decreasing variants on each cycle and satisfying the postcondition. Formally:
Theorem 1 (Safe programs execute normally).
Let  be a safe program and p a procedure in . Then:
for each valuation  if Jpre(p)K = true
then it exists a valuation 0 such that  . body(p) . 0 and Jpost(p)K0 = true
Proof: By induction in the structure of the derivations fpre(p)g body(p) fpost(p)g. See [1].
6 Postcondition Calculus
The static semantics rules of Figure 3 conform an axiomatic system to determine, given p, s and q wether or not
fpg s fqg holds. In some ocassions (such as trying to infer annotations for a procedure definition) it may probe
3

useful to infer some q such that, for a given p and s fpg s fqg holds. It is desirable that the obtained q was the
strongest to satisfy the static semantics. For decidability’s sake we will get a q that, hopefully, is strong enough
for our purpouses. We note this calculated postcondition post(s; p) = q and we formally obtain it using the rules
in Figure 4.
p j= safe(e)
post(v e; p) = 9 v0 (pbv 7! v0c ^ v = ebv 7! v0c)
(Q-ASSIGN)
p j= safe(e)
post(local v e; p) = p ^ v = e (Q-DEF) post(skip; p) = p (Q-SKIP)
post(s1; p) = r post(s2; r) = q
post(s1 s2; p) = q
(Q-SEQ)
p j= safe(g)
post(if g then s else t fi; p) = Cl9 locals(s)(post(s; p ^ g)) _ Cl9 locals(t)(post(t; p ^ :g))
(Q-IF)
true j= safe(inv) inv j= safe(g) inv j= safe(var)
p j= inv inv ^ g j= var > 0
post(var0 var s; inv ^ g) = q0
q0 j= inv q0 j= var < var0
post(while g :?! inv :# var do s od; p) = inv ^ :g (Q-WHILE)
1  i  k pbcpi 7! pic j= pre(pr)
post(call pr(cp1; : : : ; cpk); p) = 9o1;:::;ok (pbcpi 7! oic ^ post(pr)bpi 7! cpi; pi@pre 7! oic)
(Q-CALL)
Figure 4: Pest postcondition calculus
The notation Cl9V (b) refers to the existencial closure of the boolean expression b with respect to every variable
in V .
7 Precondition Calculus
Analogously to the previous section, we say that pre(s; q) = p when p is the calculated precondition of s with
respect to the boolean expression q that characterises the state after executing s. The precondition we get will
not necessarily be the weakest one. The formal rules are given in Figure 5.
pre(v e; q) = safe(e) ^ qbv 7! ec
(P-ASSIGN)
pre(skip; q) = q (P-SKIP)
pre(local v e; q) = safe(e) ^ qbv 7! ec (P-DEF)
pre(s1; r) = p pre(s2; q) = r
pre(s1 s2; q) = p
(P-SEQ)
pre(if g then s1 else s2 fi; q) = safe(g) ^ (g ^ pre(s1; q) _ :g ^ pre(s2; q))
(P-IF)
true j= safe(inv) inv j= safe(g) inv j= safe(var)
inv ^ g j= p0 p0 j= var > 0
post(var0 var s; inv ^ g) = q0
q0 j= inv q0 j= var < var0 inv ^ :g j= q
pre(while g :?! inv :# var do s od; q) = inv (P-WHILE)
1  i  k
pre(call proc(cp1; : : : ; cpk); q) = pre(proc)bpi 7! cpic ^
(9a1; : : : ; ak(post(proc)bpi 7! ai; pi@pre 7! cpic ^ qbcpi 7! aic))
(P-CALL)
Figure 5: Pest precondition calculus
References
[1] Guido de Caso. High-level iteration constructs as annotations for automated software verification.
Master’s thesis, Universidad de Buenos Aires, Tutored by Diego Garbervetsky and Daniel Gorín,
http://lafhis.dc.uba.ar/~gdecaso/tesisLicGuidodeCaso.pdf, 2007.
4