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)