Skip to content

Latest commit

 

History

History
3 lines (2 loc) · 509 Bytes

exercise-1.1.md

File metadata and controls

3 lines (2 loc) · 509 Bytes

Exercise 1.1 Extend the notion of regularity to input/output objects of a procedure, that is, to objects that are modified as well as read.

Let f be a regular procedure, and let x be an input/output object of f. Let v1 be the state of x before executing f, and let v2 be the state of x after executing f. Finally, let y be an object with state w1, where v1 is equal to w1, and let w2 be the state of y after executing f with y substituted for x as an input/output object of f. Then v2 is equal to w2.