PROC P () INITIAL INT x IS 1234: INITIAL [12]BYTE cs IS "hello, world": SEQ SEQ i = 0 FOR SIZE cs cs[i] := 'A' x := x + 1 :