Path-Aware Static Program Analyses for Specification Mining* - Mining Software Specifications: Methodologies and Applications - page 322

Syntax:
e ::= x ` j
( let x = t ` 1 in e ` ) ` 0 j
( set x := y ` 1 in e ` ) ` 0
t ::= c j x:e j x(y) j
( if x then e ` t 1 else e ` f 2 ) j
ref (x) j deref (x) j
op (x 1 ;:::;x n )

Domains:
F 2 Flow = Var+Label!AVal
v 2 AVal = P(Label+Constant+
Op(AVal :::AVal))
2 SpecMap= Label!P(Pred)
2 ProcMap= Label!Label
2 Pred =
read(Label;AVal) +write(Label;AVal)+
alloc(Label;AVal) +bind(Var;AVal)+
cbind(Var;AVal) +call(Label Label)

(` 0 ) [fbind(x;fcg)g (`)
j= F ( let x = c ` 1 in e ` ) ` 0

(Bind)

(` 0 ) [falloc(` 1 ;F(y));bind(x;` 1 )g (`)
j= F ( let x = ref (y) ` 1 in e ` ) ` 0

(Ref)

S = fwrite(` i ;F(y)) j ` i 2 F(x); ref (z) ` i 2 Pg
(` 0 ) [fSg (`)
j= F ( set x := y ` 1 in e ` ) ` 0

(Write)

(` 0 ) [fbind(x; op (F(x 1 );:::;F(x n )))g (`)
j= F ( let x = op (x 1 ;:::;x n ) ` 1 in e ` ) ` 0

(Prim)

S = fread(` i ;F(` i ));bind(x;F(` i )) j ` i 2 F(y) ^ ref (z) ` i 2 Pg
(` 0 ) [fSg (`)
j= F ( let x = deref (y) ` 1 in e ` ) ` 0

(Read)

(` 0 ) [fcbind(y;true)g (` t )
(` 0 ) [fcbind(y;false)g (` f )
` 0 [ ((` t ) \ (` f )) [fbind(x;F(` 1 ))g (`)
j= F ( let x = ( if y then e ` t 1 else e ` f 2 ) ` 1 in e ` ) ` 0

(If)

T f(` i ) j ( let z i = x i (y i ) in e i ) ` i ;` 1 2 F(x)g (` 1 )
fbind(w; v) j ( let z i = x i (y i ) in e i ) ` i ;` 1 2 F(x); v = \(F(y i ))g (` b )
(` 0 ) [fbind(x;` 1 )g (`)
j= F ( let x = (w:e ` b b ) ` 1 in e ` ) ` 0

(Abs)

S = f` j j ` i 2 F(y) ^ (w i :e i ) ` i 2 P ^e ` j j last(ei)} i )g
(` 0 ) [fcall((` 1 ) ` i ) j
` i 2 F(y) ^ (w i :e i ) ` i 2 Pg[f T f(` j ) j ` j 2 Sg[fbind(x;S)g (`)
j= F ( let x = y(z) ` 1 in e ` ) ` 0

(App)

FIGURE 9.4: Specification inference via flow analysis.