File: function_update.spec

package info (click to toggle)
mcrl2 201409.0-1
  • links: PTS, VCS
  • area: main
  • in suites: buster, jessie, jessie-kfreebsd
  • size: 46,348 kB
  • ctags: 29,960
  • sloc: cpp: 213,160; ansic: 16,219; python: 13,238; yacc: 309; lex: 214; xml: 197; makefile: 83; sh: 82; pascal: 17
file content (16 lines) | stat: -rwxr-xr-x 451 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
 
#using S
#using T

map @func_update <"function_update">: (S -> T) <"arg1"> # S <"arg2"> # T <"arg3"> -> (S -> T);

var x: S;
    y: S;
    v: T;
    w: T;
    f: S -> T;
eqn ==(f(x),v) -> @func_update(f,x,v) = f;
    @func_update(@func_update(f,x,w),x,v) = @func_update(f,x,v);
    >(x,y) -> @func_update(@func_update(f,y,w), x,v) = @func_update(@func_update(f,x,v),y,w);
    !=(x,y) -> @func_update(f,x,v)(y) = f(y);
    @func_update(f,x,v)(x) = v;