• Reducing to the basic language
  • Assertion moving
  • split statements
  • while statements
  • proc declarations
  • return statements and expressions
  • proccall statements and expressions
• Encoding the basic language in MONA
  • Guide declaration
  • Global MONA variables
  • Initial transduction predicates
  • Encoding of formula, condexp, boolexp, and lboolexp
  • Encoding of ptrexp, lptrexp, and setexp
  • Encoding of routingexp
  • Encoding of statements
  • Encoding of transductions
  • Type-correctness predicates

This section describes the translation procedure from PALE to MONA. The reader is assumed to be familiar with the basic ideas of the Pointer Assertion Logic, the PALE syntax and MONA syntax and semantics.

"T_c" denotes the type assigned to the construct c. All PALE identifiers are implicitly prefixed by "$" to avoid name clashes. Also, every 'v' variable used below stands for a fresh variable.

Reducing to the basic language

Before translating a PALE program into a MONA formula, the extension constructs are reduced to equivalent basic constructs by the following rules.

Assertion moving

For the code

if (condexp) {stm₁} {stm₂} stm₃

where stm₁ or stm₂ (or both) contain a while, split, or procedure call and stm₃ is non-empty (in which case it must begin with a while, split, or procedure call),

assert [formula] {pointerformula ...}

is inserted in both branches after stm₁ and stm₂, respectively. If stm₃ begins with a while, formula is the loop invariant; if it begins with a split, formula is the first split formula; and if it begins with a procedure call, formula is the call invariant. The pointerformulas are those associated the formula.

If {stm₂} is omitted, {} is used by default.

(The purpose of this rule is to reduce the number of required annotations.)

split statements

The code

split [formula₁] {pointerformula₁ ...} [formula₂] {pointerformula₂ ...}stm

where stm is the sequence of statements following the split statement (until the end of the innermost enclosing if branch, or the end of the current transduce) is replaced by

assert [formula₁] {pointerformula₁ ...}

and a new transduce is added:

transduce [formula₂] {pointerformula₂ ...}
stm

If [formula₂] is omitted, formula₁ is used in place of formula₂. If [formula₂] is present, a warning is generated because validity of formula₂ in general cannot be verified (i.e. the rule is unsound).

while statements

The code

while [formula] {pointerformula ...} (condexp) {stm} stm'

where stm' is the sequence of statements following the while statement (until the end of the innermost enclosing if branch, or the end of the current transduce) is replaced by

assert [formula] {pointerformula ...}

and two new transduces are added:

transduce [formula & condexp] {pointerformula ...}
stm
assert [formula] {pointerformula ...}

transduce [formula & !condexp] {pointerformula ...}
stm'

proc declarations

The code

proc n(progvar₁, progvar₂, ...):T
logicvar₁; logicvar₂; ...
[formula₁] {pointerformula₁ ...}
{
  progvar'₁; progvar'₂; ...
  stm
}
[formula₂] {pointerformula₂ ...}

is replaced by

pointer _n__return:T;
progvar₁, progvar₂, ..., progvar'₁; progvar'₂; ...   (where each variable is renamed from v to _n_v)

transduce logicvar₁; logicvar₂; ... [formula₁ & progvar'₁=null & progvar'₂=false & ...] {pointerformula₁ ...}
              (assuming progvar'₁ is a data or pointer and progvar'₂ is a bool)
stm
assert [formula₂] {pointerformula₂ ...}

pred _n__pre(progvar₁, progvar₂, ..., logicvar₁, logicvar₂, ...) = formula₁;

pred _n__post(logicvar₁, logicvar₂, ...) = formula₂;

All data variables in _n__pre(...) are changed to pointer variables, and all references to the arguments and local variables in stm are replaced by their new names.

If the return type is bool instead of a type T, then "bool _n__return" is used instead of "pointer _n__return:T". If the return type is void, the variable is omitted.

If the procedure body is omitted (i.e. the declaration is a procedure prototype declaration), the transduce is not generated.

return statements and expressions

The statement

return progexp;

occuring in the procedure n is replaced by

_n__return = progexp;

The expression

return

occuring in the procedure n is replaced by

_n__return

proccall statements and expressions

The code

lprogexp = n(progexp₁, progexp₂, ...) [formula]; stm

where stm is the sequence of statements following the procedure call statement (until the end of the innermost enclosing if branch, or the end of the current transduce) is replaced by

assert [QUANTIFY formula & _n__pre(progexp₁, progexp₂, ..., logicvar₁, logicvar₂, ...)] {pointerformula_pre ...}

where logicvar₁, logicvar₂, ... are the names of the logical variables of the procedure n prefixed by _n___, and a new transduce is added:

transduce [QUANTIFY formula & _n__post(logicvar₁, logicvar₂, ...)] {pointerformula_post ...}
lprogexp = _n__return;
stm

The pointerformulas are those from the procedure being called.

Every occurence of n.p, n.b, and n.s in formula is replaced by _n___p, etc. QUANTIFY is a list of existential quantifiers of logicvar₁, logicvar₂, ... (again prefixed by _n___) of the appropriate types (see EXISTSLOGICVARS below).

If "lprogexp = " is omitted, the assignment is to lprogexp is omitted.

Every "?" occuring as an actual parameter is replaced by _choice_i (where i is the number of the occurence) declared globally by "var0 _choice_i;".

Encoding the basic language in MONA

A desugared PALE program is translated into MONA formulas by 1) making the guide declaration and global variables, 2) initialising the transduction predicates, and 3) encoding each transduce as described below.

The encoding of expressions is relative to a "current" set of store predicates, indexed by z. The store predicates are those shown below under "initial transduction predicates".

Guide declaration

Declaration of the Guided Tree Automaton guide (the guide places for each data variable an instances of the its type in the infinite binary tree) and emulation of M2L-Tree:

ws2s;
guide boolss->(top_1,dummy1),
  top_1->(T_d1,top_2), ..., top_n-1->(T_dn-1,T_dn),   (for each data variable d of type T_d)
  T_i->(T_di,1,T_i_1), ..., T_i_m-1->(T_di,m-1,T_di,m), ...,   (for all data fields d_i,j in T_i and for all T_i used by a data variable)
  dummy1->(dummy1,dummy1),
  dummy2->(dummy2,dummy2);   (used when less than 2 data variables or less than 2 data fields)
universe univ:0,dummyuniv:1;

var2 [top_1,...,top_n-1,T_d1, ..., T_dn] $ where all1 p: (p in $) => ((p^ in $) | (p^=p));
allpos $;
defaultwhere2(P) = P sub $;

Global MONA variables

Pointer encoding:

pred ptr(var2 X) = X sub $ & (all1 [X] p,q: p in X & q in X => p=q);
pred null(var2 X) = empty(X);

Variables for encoding the initial store:

var2 [T_p] _ptr_p where ptr(_ptr_p);     (for each pointer variable p)
var0 _bool_b;     (for each bool variable b)
var2 [T_s] _set_s;     (for each set variable s)
var2 [T_b] _bool_T_b;     (for each bool field b in some type T)

Nondeterministic choices:

var0 _choice_i;     (for each occuring '?' (where i is its number)

Initial transduction predicates

Encoding of the initial store ("path of" is the path corresponding to the guide encoding and "p-path" is a unique path leading to a root state-space of the appropriate type):

pred bool_T_b_z(var2 v where ptr(v)) = v sub _bool_T_b;     (for each bool field b in some type T)

pred succ_T_p_z(var2 v1 where ptr(v1), var2 v2 where ptr(v2)) = v1.<path of T.p> inter $=v2;     (for each data field p in some type T)
pred null_T_p_z(var2 v where ptr(v)) = ~v.<path of T.p> sub $;     (for each data field p in some type T)

pred succ_T_p_z(var2 this where ptr(this), var2 p where ptr(p)) = [[formula]]_z;     (for each pointer field p associated formula in some type T)
pred null_T_p_z(var2 this where ptr(this)) =
  ex2 [T_p] p where ptr(p): succ_T_p_z(this,p) & null(p);     (for each pointer field p in some type T)

pred ptr_p_z(var2 v where ptr(v)) =
  (null(v)<=>root(univ).<p-path> notin $) & (~null(v)<=>root(univ).<p-path> in v);     (for each data variable p)

pred ptr_p_z(var2 v) = _ptr_p=v;     (for each pointer variable p)

pred bool_b_z() = _bool_b;     (for each bool variable b)

pred memfailed_z() = false;

"formula" refers to the pre-condition pointer formula in the current transduce for the appropriate pointer field, or if no such formula, to the "default" pointer field formula specified in the type declaration.

(The M2L-Tree variable '$' determines the extent of the backbone; data variables are universes; boolean fields and sets are represented by second-order MONA variables; pointer variables are empty or singleton second-order variables; and boolean variables in PALE become boolean variables in MONA.)

Encoding of formula, condexp, boolexp, and lboolexp

"[[c]]_z" denotes the MONA encoding of the PALE formula, condexp, boolexp, or lboolexp construct c:

[[?]]_z  =  _choice_i     (where i is the number of the "?")
[[existpos p of T: formula]]_z  =  ex2 [T] p where ptr(p): ~null(p) & [[formula]]_z
[[allpos p of T: formula]]_z  =  all2 [T] p where ptr(p): ~null(p) => [[formula]]_z
[[existset s of T: formula]]_z  =  ex2 [T] s: [[formula]]_z
[[allset s of T: formula]]_z  =  all2 [T] s: [[formula]]_z
[[existptr p of T: formula]]_z  =  ex2 [T] p where ptr(p): [[formula]]_z
[[allptr p of T: formula]]_z  =  all2 [T] p where ptr(p): [[formula]]_z
[[existbool b: formula]]_z  =  ex0 b: [[formula]]_z
[[allbool b: formula]]_z  =  all0 b: [[formula]]_z
[[! formula]]_z  =  ~[[formula]]_z
[[formula1 & formula2]]_z  =  [[formula1]]_z & [[formula2]]_z
[[formula1 | formula2]]_z  =  [[formula1]]_z | [[formula2]]_z
[[formula1 => formula2]]_z  =  [[formula1]]_z => [[formula2]]_z
[[formula1 <=> formula2]]_z  =  [[formula1]]_z <=> [[formula2]]_z
[[ptrexp in setexp]]_z  =  ex2 [T_ptrexp] v1 where ptr(v1): ex2 [T_setexp] v2: v1 sub v2 & ~null(v1) & [[ptrexp]]_z(v1) & [[setexp]]_z(v2)
[[setexp1 sub setexp2]]_z  =  ex2 [T_setexp1] v1: ex2 [T_setexp2] v2: v1 sub v2 & [[setexp1]]_z(v1) & [[setexp2]]_z(v2)
[[setexp1 = setexp2]]_z  =  ex2 [T_setexp1] v1: ex2 [T_setexp2] v2: v1=v2 & [[setexp1]]_z(v1) & [[setexp2]]_z(v2)
[[setexp1 != setexp2]]_z  =  ~[[setexp1 = setexp2]]_z
[[ptrexp1 = ptrexp2]]_z  =  NULL(ptrexp2)   if ptrexp1 is null
                            = NULL(ptrexp1)   otherwise, if ptrexp2 is null
                            = ex2 [T_ptrexp1] v1 where ptr(v1): ex2 [T_ptrexp2] v2 where ptr(v2):
                             v1=v2 & [[ptrexp1]]_z(v1) & [[ptrexp2]]_z(v2)   otherwise
[[ptrexp1 != ptrexp2]]_z  =  ~[[ptrexp1 = ptrexp2]]_z
[[boolexp1 = boolexp2]]_z  =  [[boolexp1]]_z <=> [[boolexp2]]_z
[[boolexp1 != boolexp2]]_z  =  ~[[boolexp1 = boolexp2]]_z
[[empty ( setexp )]]_z  =  ex2 [T_setexp] v: empty(v) & [[setexp]]_z(v)
[[ptrexp1 < routingexp > ptrexp2]]_z  =  ex2 [T_ptrexp1] v1 where ptr(v1): ex2 [T_ptrexp2] v2,v3 where ptr(v3):
    v3 sub v2 & (null(v1) <=> null(v3)) & [[ptrexp1]]_z(v1) & [[ptrexp2]]_z(v3) & [[routingexp]]_z(v1,v2)
[[ptrexp < routingexp > setexp]]_z  =  ex2 [T_ptrexp] v1 where ptr(v1): ex2 [T_setexp] v2:
    [[ptrexp]]_z(v1) & [[setexp]]_z(v2) & [[routingexp]]_z(v1,v2)
[[formula₁ ? formula₂ : formula₃]]_z = ex0 t: (t<=>[[formula₁]]_z) & (t=>[[formula₂]]_z) & (~t=>[[formula₃]]_z)
[[m ( ptrexp1, boolexp2, setexp3, ... )]]_z  = 
    ex2 [T_ptrexp1] v1 where ptr(v1): [[ptrexp1]]_z(v1) &
    ex0 v2: (v2<=>[[boolexp2]]_z) &
    ex2 [T_setexp3] v3: [[setexp3]]_z(v3) &
    ... &
    ex2 [T_f1] f1 where ptr(f1): f1=v1 &
    ex0 f2: (f2<=>v2) &
    ex2 [T_f3] f3: f3=v3 &
    ... & [[body]]_z   (where body is the body of m and f1, f2, f3, ... are the formal parameters of type pointer, bool, set, ..., respectively)
[[true]]_z  =  true
[[false]]_z  =  false
[[b]]_z  =  bool_b_z()   if b refers to a global MONA declaration
       =  b         if b refers to a quantifier
[[ptrexp . b]]_z  =  ex2 [T_ptrexp] v where ptr(v): bool_T_v_b_z(v) & ~null(v) & [[ptrexp]]_z(v)

Encoding of ptrexp, lptrexp, and setexp

"[[c]]_z(v)" here denotes the MONA encoding of the PALE ptrexp, lptrexp, or setexp construct c, with its value bound to the variable v:

[[s]]_z(v)  =  _set_s=v   if s refers to a global MONA declaration
         =  s=v         if s refers to a quantifier
[[p]]_z(v)  =  ptr_p_z(v)   if p refers to a global MONA declaration
         =  p=v         if p refers to a quantifier
[[this]]_z(v)  =  this=v   (same for pos)
[[null]]_z(v)  =  null(v)
[[ptrexp . p]]_z(v)  =  ex2 [T_ptrexp] v' where ptr(v'): succ_T_v_p_z(v',v) & ~null(v') & [[ptrexp]]_z(v')
[[ptrexp ^ T . p]]_z(v)  = 
    all2 [T_v] v'' where ptr(v''): ~null(v'') =>
      (v'' sub v <=> ex2 [T_ptrexp] v' where ptr(v'): ~null(v') & [[ptrexp]]_z(v') & succ_T_p_z(v'',v'))
[[formula ? ptrexp₁ : ptrexp₂]]_z(v) = ex0 t: (t<=>[[formula]]_z) & (t=>[[ptrexp₁]]_z(v)) & (~t=>[[ptrexp₂]]_z(v))
[[formula ? setexp₁ : setexp₂]]_z(v) = ex0 t: (t<=>[[formula]]_z) & (t=>[[setexp₁]]_z(v)) & (~t=>[[setexp₂]]_z(v))
[[{ ptrexp1,... }]]_z(v)  =  ex2 [T_ptrexp1] v1 where ptr(v1): [[ptrexp1]]_z(v1) & ... & v=v1 union ...
[[setexp1 union setexp2]]_z(v)  =  ex2 [T_setexp1] v1: ex2 [T_setexp2] v2: v=v1 union v2 & [[setexp1]]_z(v1) & [[setexp2]]_z(v2)
[[setexp1 inter setexp2]]_z(v)  =  ex2 [T_setexp1] v1: ex2 [T_setexp2] v2: v=v1 inter v2 & [[setexp1]]_z(v1) & [[setexp2]]_z(v2)
[[setexp1 minus setexp2]]_z(v)  =  ex2 [T_setexp1] v1: ex2 [T_setexp2] v2: v=v1 \ v2 & [[setexp1]]_z(v1) & [[setexp2]]_z(v2)

Encoding of routingexp

"[[c]]_z(v1,v2)" denotes the MONA encoding of the PALE routingexp c, with its begin and end values bound to the variables v1 and v2, respectively:

[[p]]_z(v1,v2)  =  DOWN(v1,v2,p) & all2 [T_p] v: DOWN(v1,v,p) => v2 sub v
[[^ T . p]]_z(v1,v2)  =  UP(v1,v2,p) & all2 [T_p] v: UP(v1,v,p) => v2 sub v
[[[ formula ]]]_z(v1,v2)  =  all2 [T_v1] pos where ptr(pos): ~null(pos) => (pos sub v2 <=> pos sub v1 & [[formula]]_z)
[[routingexp1 . routingexp2]]_z(v1,v2)  =  ex2 [T_routingexp1] v: [[routingexp1]]_z(v1,v) & [[routingexp2]]_z(v,v2)
[[routingexp1 + routingexp2]]_z(v1,v2)  =  ex2 [T_routingexp1] v,v': v2=v union v' & [[routingexp1]]_z(v1,v) & [[routingexp2]]_z(v1,v')
[[routingexp *](v1,v2)  =  STAR(routingexp,v1,v2) & ~ex2 [T_routingexp] v: STAR(routingexp,v1,v) & v sub v2 & v~=v2

DOWN(src,dst,p) =  all2 [T_src] v1 where ptr(v1): ~null(v1) & v1 sub src & ~null_T_src_p_z(v1) =>
      ex2 [T_dst] v2 where ptr(v2): ~null(v2) & v2 sub dst & succ_T_src_p_z(v1,v2)
UP(src,dst,p) =  all2 [T_src] v1 where ptr(v1): ~null(v1) & v1 sub src =>
      all2 [T_dst] v2 where ptr(v2): ~null(v2) & succ_T_dst_p_z(v2,v1) => v2 sub dst
STAR(routingexp,src,dst) =  src sub dst & all2 [T_routingexp] v1,v2: v1 sub dst & [[routingexp]]_z(v1,v2) => v2 sub dst

Encoding of statements

Each statement is encoded as a predicate transformer by updating certain store predicates (z and z' denote the "before" and "after" store predicate indices, respectively; those predicates that are not mentioned are unchanged):

Sequence:

stm1 stm2:

If z'' denotes the store predicate index after transducing stm1 starting from z, then z' is the store predicate index after transducing stm2 starting from z''.

Assignment:

A multi-assignment (i.e. a comma-separated list of assignments) is encoded as if it was a statement sequence, except that the individual assignments all are evaluated with respect to the original store predicate index z.

p = ptrexp:

pred memfailed_z'() = memfailed_z() | NULLDEREF(ptrexp);
pred ptr_p_z'(var2 v where ptr(v)) = [[ptrexp]]_z(v);

b = condexp:

pred memfailed_z'() = memfailed_z() | NULLDEREF(condexp);
pred bool_b_z'() = [[condexp]]_z;

ptrexp1.p = ptrexp2:

pred memfailed_z'() = memfailed_z() | NULLDEREF(ptrexp1.p) | NULLDEREF(ptrexp2);
pred succ_T_ptrexp1_p_z'(var2 v1 where ptr(v1), var2 v2 where ptr(v2)) =
    IF [[ptrexp1]]_z(v1) THEN [[ptrexp2]]_z(v2) ELSE succ_T_ptrexp1_p_z(v1,v2);
pred null_T_ptrexp1_p_z'(var2 v where ptr(v)) =
    IF [[ptrexp1]]_z(v) THEN NULL(ptrexp2) ELSE null_T_ptrexp1_p_z(v);

ptrexp.b = condexp:

pred memfailed_z'() = memfailed_z() | NULLDEREF(ptrexp.b) | NULLDEREF(condexp);
pred bool_T_ptrexp_b_z'(var2 v where ptr(v)) =
    IF [[ptrexp]]_z(v) THEN [[condexp]]_z ELSE bool_T_ptrexp_b_z(v);

Assertion:

assert [formula] { pointerformula ... }:

pred assertfailed_z'(DECLLOGICVARS) = assertfailed_z(LOGICVARS) | ~[[formula]]_z | ~POINTERSTYPECORRECT;

The pointerformulas specify formulas which override the defaults in the type declarations. If a pointerformula is specified without a formula, that pointer field is skipped.

Conditional:

if (condexp) {stm1} {stm2}:

pred memfailed_z'() = memfailed_z() | NULLDEREF(condexp);
pred branch_i() = [[condexp]]_z;
  (where i is the number of the conditional)

Let z1 and z2 denote the store predicate indices obtained by performing predicate transformation of stm1 and stm2, respectively, starting from index z.

pred memfailed_z'() =
    IF branch_z() THEN memfailed_z1() ELSE memfailed_z2();
pred assertfailed_z'(DECLLOGICVARS) =
    IF branch_z() THEN assertfailed_z1(LOGICVARS) ELSE assertfailed_z2(LOGICVARS);
pred ptr_p_z'(var2 t where ptr(t)) =
    IF branch_z() THEN ptr_p_z1(t) ELSE ptr_p_z2(t);     (for each pointer or data variable p)
pred bool_b_z'() =
    IF branch_z() THEN bool_b_z1() ELSE bool_b_z2();     (for each bool variable b)
pred bool_T_b_z'(var2 t where ptr(t)) =
    IF branch_z() THEN bool_T_b_z1(t) ELSE bool_T_b_z2(t);     (for each bool field b in some type T)
pred succ_T_p_z'(var2 t1 where ptr(t1), var2 t2 where ptr(t2)) =
    IF branch_z() THEN succ_T_p_z1(t1,t2) ELSE succ_T_p_z2(t1,t2);     (for each pointer or data field d in some type T)
pred null_T_p_z'(var2 t where ptr(t)) =
    IF branch_z() THEN null_T_p_z1(t) ELSE null_T_p_z2(t);     (for each pointer or data field p in some type T)

Abbreviations used above:

                / null(p)   if ptrexp is a quantified variable p
               /  ex2 [T_p] t where ptr(t): null(t) & ptr_p_z(t)   if ptrexp is a global pointer or data variable p
NULL(ptrexp) = <   ex2 [T_ptrexp'] v where ptr(v): null_T_ptrexp'_p_z(v) & [[ptrexp']]_z(v)   if ptrexp is ptrexp'.p
               \  true   if ptrexp is null
                \ false   otherwise

                    / NULLDEREF(ptrexp) | NULL(ptrexp)   if exp is ptrexp.p
                   /  NULLDEREF(exp₁) | NULLDEREF(exp₂) & [[exp₁]]_z   if exp is exp₁ & exp₂
                  /   NULLDEREF(exp₁) | NULLDEREF(exp₂) & ~[[exp₁]]_z   if exp is exp₁ | exp₂
NULLDEREF(exp) = <    NULLDEREF(exp₁) | NULLDEREF(exp₂) & [[exp₁]]_z   if exp is exp₁ => exp₂
                  \   NULLDEREF(exp₁) | NULLDEREF(exp₂)   if exp is exp₁ <=> exp₂
                   \  NULLDEREF(exp')   if exp is !exp'
                    \ false   otherwise

IF formula1 THEN formula2 ELSE formula3 =
    ex0 t: (t<=>formula1) & (t=>formula2) & (~t=>formula3)

Encoding of transductions

The following MONA code is generated for each occurence of

transduce logicvars [formula] stm

w is the number of the transduction, z is a unique initial store predicate index, and z' is the store predicate index obtained by performing a transduction on stm starting from z. (The initial store predicates defined above are shared for all transductions, the assertfailed predicate initialized below is defined separately for each transduction.)

pred assertfailed_z(DECLLOGICVARS) = false;

Translate the transduce formula:

pred precond_w(DECLLOGICVARS) = [[formula]]_z;   (where formula is the transduce formula)

pred precondsat_w() = EXISTSLOGICVARS precond_w(LOGICVARS);

Verify that the transduce formula is satisfiable, that there can be no null pointer dereferences, that the pointer field formulas are valid, that the backbone does not contain cycles, that the data variables are disjoint and span the same cells as before execution, and that the assertions are satisfied:

verify precondsat_w();

verify precondsat_w() => ~memfailed_w();

verify precondsat_w() => nocycles1_w() & nocycles2_w();

verify precondsat_w() => datadisjoint_w();

verify precondsat_w() => datacomplete_w();

verify FORALLLOGICVARS precond_w(LOGICVARS) => ~assertfailed_w(LOGICVARS);

Abbreviations used above:

DECLLOGICVARS: for each logical variable in the transduce, a comma-separated list of:
  var2 p where ptr(p)   (for pointer variables p)
  var0 b   (for boolean variables b)
  var2 s   (for set variables s)

LOGICVARS = v₁,...,v_n   (for all logical variables v₁,...,v_n in the transduce)

FORALLLOGICVARS = for each logical variable in the transduce:
  all2 [T] p where ptr(p):   (for pointer variables p of type T)
  all0 b:   (for boolean variables b)
  all2 [T] s:   (for set variables s of type T)

EXISTSLOGICVARS = for each logical variable in the transduce:
  ex2 [T] p where ptr(p):   (for pointer variables p of type T)
  ex0 b:   (for boolean variables b)
  ex2 [T] s:   (for set variables s of type T)

The following checks well-formedness of a pointer field formula p in a type T:

verify all2 [T] this: ~null(this) =>
  (all2 [T_p] p,p': formula_T_p_w(this,p) & formula_T_p'_w(this,p') => p=p') &
  ex2 [T_p] p: formula_T_p_w(this,p);

formula_T_p_w(this,p) is true for a pointer field p in a type T if the associated formula is satisfied in a store z:

pred formula_T_p_w(var2 this where ptr(this), p where ptr(p)) = [[formula]]_z

Type-correctness predicates

Each transduction is associated the following predicates (where w is the number of the transduction and z is the final store predicate index of the transduction).

reachable(R) is true if R is the set of heap positions which are reachable in zero or more steps from the used global data and pointer variables:

pred containreachable_w(var2 R) =
  (ex2 [T_p] t: ptr_p_z(t) & t sub R) & ... (for every global data and pointer variable p used in the current transduction)
  (all2 [T] t where ptr(t): ~null(t) & t sub R =>
    (~null_T_p_z(t) => ex2 [T_p] t' where ptr(t'): ~null(t') & succ_T_p_z(t,t') & t' sub R) & ... (for every data and pointer field p in T)
  ) & ... ;   (for every type T)

pred reachable_w(var2 R) = containreachable_w(R) & ~ex2 R': containreachable_w(R') & R' sub R & R'~=R;

datareachable(R) is true if R is the set of heap positions which are reachable in zero or more data-field steps from the global data variables:

pred containdatareachable_w(var2 R) =
  (ex2 [T_p] t: ptr_p_z(t) & t sub R) & ... (for every global data variable p)
  (all2 [T] t where ptr(t): ~null(t) & t sub R =>
    (~null_T_p_z(t) => ex2 [T_p] t' where ptr(t'): ~null(t') & succ_T_p_z(t,t') & t' sub R) & ... (for every data field p in T)
  ) & ... ;   (for every type T)

pred datareachable_w(var2 R) = containdatareachable_w(R) & ~ex2 R': containdatareachable_w(R') & R' sub R & R'~=R;

reachablefrom(t,R) is true if R is the set of heap positions which are reachable from t in one or more data-field steps:

pred containreachablefrom_w(var2 tt where ptr(tt), var2 R) =
  (all2 [T] t where ptr(t): ~null(t) & (t=tt | t sub R) =>
    (~null_T_p_z(t) => ex2 [T_p] t' where ptr(t'): ~null(t') & succ_T_p_z(t,t') & t' sub R) & ... (for every data field p in T)
  ) & ... ;   (for every type T)

pred reachablefrom_w(var2 tt where ptr(tt), var2 R) =
  containreachablefrom_w(tt,R) &
  ~ex2 R': containreachablefrom_w(tt,R) & (containreachablefrom_w(tt,R') & (R' sub R & R'~=R;))

nocycles1() is true if there is no reachable heap position which is reachable from itself in one or more data-field steps:

pred nocycles1_w() = all2 [T1,T2,...] R: reachable_w(R) =>   (where T1,T2,... are all declared types)
  (all2 [R] t where ptr(t): ~null(t) & t sub R => all2 [R] R': reachablefrom_w(t,R') => ~(t sub R'));

nocycles2() is true if every two data fields in the same reachable cell can reach disjoint sets of cells:

pred nocycles2_w() = all2 [T1,T2,...] R: reachable_w(R) =>   (where T1,T2,... are all declared types)
  ...

datadisjoint() is true if the used data variables refer to disjoint graph type backbones:

pred datadisjoint_w() =
  (all2 [T1,T2,...] R: (ex2 [T_p] t: ~null(t) & ptr_p_z(t) & reachablefrom_w(t,R)) =>
    (all2 [T1,T2,...] R': (ex2 [T_p] t: ~null(t) & ptr_p'_z(t) & reachablefrom_w(t,R')) =>
      empty(R,R'))) & ... ;   (for every pair of distinct data variables p,p' used in the current transduction)

datacomplete() is true if the cells reachable from data variables are the same as before executing the transduction code:

pred datacomplete_w() =
  all2 [T1,T2,...] R,S: datareachable_w(R) & S sub $ => S sub R;

POINTERSTYPECORRECT is true if all pointer field formulas are satisfied for all reachable positions:

POINTERSTYPECORRECT =
  all2 [T1,T2,...] R: reachable_w(R) =>   (where T1,T2,... are all declared types)
  (all2 [T] this where ptr(this): ~null(this) & this sub R =>
   (all2 [T_p] p where ptr(p): (succ_T_p_z(this,p) & ~null_T_p_z(this) | null(p) & null_T_p_z(this)) <=> [[formula]]_z) & ...
        (for every pointer field p associated formula)
  ) & ... ;   (for every type T)

reachable2 is as reachable above, but tied to an assert instead of a transduce:

pred containreachable2_j(var2 R) =
  (ex2 [T_p] t: ptr_p_z(t) & t sub R) & ... (for every global data and pointer variable p used in the current transduction)
  (all2 [T] t where ptr(t): ~null(t) & t sub R =>
    (~null_T_p_z(t) => ex2 [T_p] t' where ptr(t'): ~null(t') & succ_T_p_z(t,t') & t' sub R) & ... (for every data and pointer field p in T)
  ) & ... ;   (for every type T)

pred reachable2_j(var2 R) = containreachable2_j(R) & ~ex2 R': containreachable2_j(R') & R' sub R & R'~=R;