Translation of Method Parameters

  • In-parameter x (i.e., a normal call-by-value parameter) is translated into x$in for the corresponding parameter of the procedure (and is the variable used in pre- and postconditions). It also generates a local variable for the procedure (also named x). At the beginning of the implementation, the assignment "x := x$in" is generated. All occurrences of the parameter in the method body are translated into occurrences of "x". That way, if the method body happens to assign to the parameter, those become assignments to the local (since in Boogie in parameters cannot be written to).
  • Ref-parameter x is translated into x$in for the corresponding parameter of the procedure. It also generates an out parameter for the procedure named x$out. At the beginning of the implementation the assignment "x$out := x$in" is generated. All occurrences of the parameter in the method body are translated into occurrences of "x$out".
  • Out-parameter x is translated into an out-parameter of the procedure. All occurrences of the parameter in the method body are translated into occurrences of "x$out".

Last edited Jul 6, 2010 at 2:25 AM by mikebarnett, version 1

Comments

No comments yet.