[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Question Concerning functions

If I call a function that changes a variable do I then reference the updated variable?
for example:

L5(c: L_Graph, x: Entity):L_Graph = c with [Node:= Node_update(c`Node, x, c`Node(x)`e1`1, c`Node(x)`e1`2), three:= c`Node(x)`dest]
Node_update will update X's destination node, which I then want to store in my constant three. Do I get the updated node?


Boo! Scare away worms, viruses and so much more! Try Windows Live OneCare! Try now!