CSC195, Class 44: Semantics of Procedures

Overview:
* What is a (non-recursive) procedure?
* Gries-style procedure declarations.
* Informal meaning of procedure calls.
* Formal meaning of procedure calls.

Notes:
* No outline; too busy answering questions
* We may have prospectives visiting (unlikely)
* Info about cool independent
* Homework rescheduled until Tuesday.

What is a procedure?
* A way of getting other information from information.
  Convert values to values.
* Collection of instructions that tells the computer
  how to do some task.
* Named (at least in many languages)
* May be parameterized

Basic structure

proc NAME ( PARAMETER-LIST )
  SEQUENCE-OF-INSTRUCTIONS

Insert logic

proc NAME ( PARAMETER-LIST )
  { P } SEQUENCE-OF-INSTRUCTIONS { Q }

Three kinds of parameters:
* Value: Don't change
* Result: Only returned
  In C: x = foo(bar);
  In Gries: foo(bar,x);
* Third kind: value/result
  Input, may change

Two thoughts on parameters that may change

(1) Any changes to the formals during the procedure
  are independent of the actual until after the procedure
  exits.
(2) Any changes to the formals during the procedure
  also change the actuals.

global x: int;

foo(value result bar: int)
{
  bar := bar+1;
  print(x);
  print(bar);
}

x := 1;
foo(x);
print(x);

OUTPUT
  1  ; x within procedure
  2  ; bar within procedure
  2  ; x after procedure

Variable parameters are a lot like value-result parameters,
except that the memory for the two is shared.

foo(variable bar: int)

...

OUTPUT

  2: x within procedure
  2: bar within procedure
  2: x after procedure

Argument for value-result:
* It can be difficult to understand what's happening with
  when there are lots of changes unless you localize the
  changes.
* It is therefore difficult to analyze procedures with
  variable parameters.

Argument for variable parameters:
* Might be easier to switch a variable between processes:
* Copying is expensive and value-result does a lot of
  copying.
* Gries likes value-result.

----------------------------------------

proc NAME ( value-params, result-params, value-result-parms)
  { P } SEQUENCE-OF-INSTRUCTIONS { Q }

value params: as
result params: bs
value-result params: cs

How do P and Q relate to the rest of the procedure?
  P needs to be true in order for the procedure to operate
  Q is true after the procedure terminates
   Q should only refer to result-params and value-result-params

We know that Q is true afterwards by proving that

  P is in wp(SOI,Q)

It is your responsibility as programmer to prove this.

Why would proving that be useful?
* We know our procedure is correct (provided our proof
  is correct).
* Might help you figure out appropriate preconditions.
* If you're proving a big program correct, it's nice to
  prove little bits at a time.  (Procedures provide
  lemmas for the proof-of-correctness of the program.)

Suppose we've defined a procedure, p(As,Bs,Cs) with
precondition P and postcondition Q what can
we say about

   wp(p(Xs,Ys,Zs), R)

When is R true?
  When R depends only on the value parameters of p and
  P implies R

sort(value-result values: int[])
  { values = V } asdfasdfads { perm(values,V), inorder(values) }

  sort(stuff);
  { stuff[0] is the smallest value in stuff }
  print(stuff[0]);

We'd like (approximately)

  substitute(Ys,Zs for Bs,Cs in Q) => R

In order for that to hold, the appropriate P must hold

  substitute(Xs,Ys for As,Bs in P)
* We need to think about substitution

   substitute(Xs,Ys for As,Bs in ) and
   (substitute(Ys,Zs for Bs,Cs in Q) => R)
   is in
   wp(p(Xs,Ys,Zs), R)