Function definitions - roboguy13/suslik GitHub Wiki

Inspired in part by the difficulties with composition of "specification functions".

Consider a new language construct for defining functions (in the sense of the "predicates-as-functions" functional style that we have been working with). Note that result is a new reserved word in the context of this construct, representing the "result" of the "function." Another new syntax is introduced to "access" the result of function application: a new heaplet form x = f(y). [1]

function map(set preS, set postS, pred p): loc {
| result == null => { preS =i {} && postS =i {} ; emp }
| not (result == null) => {
    preS =i {v} ++ preS1 && postS =i {r} ++ postS1 && p(v, r)
      ;
    [result, 2] ** result :-> r ** (result + 1) :-> nxt ** nxt = map(preS1, postS1, p)
  }
}

Side-note: There is a bidirectional flow of information here. Information from the result is used by the function, but the function also provides additional, new information about the result. Is this another manifestation of the relational nature of the functional-style SuSLik specifications?

This could be transformed into

predicate map(loc x, set preS, set postS, pred p) {
| x == null        => { preS =i {} && postS =i {} ; emp }
| not (x == null)  => {
    preS =i {v} ++ preS1 && postS =i {r} ++ postS1 && p(v, r)
      ;
    [x, 2] ** x :-> r ** (x + 1) :-> nxt ** map(nxt, preS1, postS1, p)
  }
}

The purpose of the function construct is to specify the "out parameter" to make it much easier to accomplish the sort of composition mentioned here and get a function composition syntax that looks like the "pseudo-SuSLik" examples given here. The transformation from here could be used to implement composition, but the function construct should make the interface exposed to the programmer much easier to use and read.

Using the notation from the other page, a function composition like this in a specification:

{ ... }
void example(loc x)
{ ... ; r = f(g(x, y), z) ** ... }

(where f and g are defined as functions)

would be the same as this, written in the other notation:

{ ... }
void example(loc x)
{ ... ; join(g(r, x, y), f(r, z)) ** ... }

[1]: (is this necessary? Should we just use (result + 1) :-> map(preS1, postS1, p) below, or does the = syntax give other benefits, like a kind of let-binding?)

Composition example

function fold(loc x, set s, int z, pred p): int {
|  x == null => { result == z ; emp }
|  not (x == null) => {
    s =i {v} ++ s1 && p(result, v, acc1)
      ;
    [x, 2] ** x :-> v ** (x + 1) :-> nxt ** fold(nxt, s1, acc1, z, p)
  }
}

function map(set preS, set postS, pred p): loc {
| result == null => { preS =i {} && postS =i {} ; emp }
| not (result == null) => {
    preS =i {v} ++ preS1 && postS =i {r} ++ postS1 && p(v, r)
      ;
    [result, 2] ** result :-> r ** (result + 1) :-> nxt ** nxt = map(preS1, postS1, p)
  }
}

{ sll(x, preS) ** y :-> 0 }
void composition_example(loc x, loc y)
{ y :-> r
   ** r = fold(x
              ,map(preS, postS, pred(oldV, newV) => newV == 10*oldV)
              ,postS
              ,0
              ,pred(updated, v, acc) => updated == v+acc) }

"Unifying" the pure parts of the corresponding branches of the two predicate functions and "merging" the spatial parts of the two predicate functions (by trying to combine them and favoring the outermost function's spatial part when there is a conflict), we get:

predicate fold.map(int res, loc x, set preS, set postS, int z, pred fold.p, pred map.p) {
| x == null => { preS =i {} && postS =i {} && result == z ; emp }
| not (x == null) => {
    preS =i {v} ++ preS1 && postS =i {r} ++ postS1
    && map.p(v, r)
    && fold.p(res, r, acc1)
      ;
    [x, 2] ** x :-> r ** (x + 1) :-> nxt ** fold.map(res, nxt, preS1, postS1, acc1, z, fold.p, map.p)
  }
}


{ sll(x, preS) ** y :-> 0 }
void composition_example(loc x, loc y)
{ y :-> r
   ** fold.map(r
              ,x
              ,preS
              ,postS
              ,0
              ,pred(updated, v, acc) => updated == v+acc)
              ,pred(oldV, newV) => newV == 10*oldV) }
⚠️ **GitHub.com Fallback** ⚠️