5.1. Transparent procedures🔗

Laurel procedures are transparent by default, meaning that a call can use the body of the callee to prove facts about the result of the call. Laurel aims to allow any procedure to be transparent; some restrictions still remain for now. In particular, Laurel will allow procedures that contain loops or that modify the heap to be transparent as well.

By allowing any procedure to be transparent, Laurel prevents users from having to repeat the body of a procedure in a postcondition. Here's an example that shows an opaque procedure that would have been easier to define as being transparent, without any loss of readability:

procedure increment(counter: Counter)
  // In Laurel, the next three lines can be left out and callers will get the same information
  opaque
  modifies counter
  ensures counter#value == old(counter#value) + 1
{
  counter#value := counter#value + 1
};