DIRECTORY BitOps, Rope; EUProofs: CEDAR PROGRAM IMPORTS BitOps = BEGIN Mask: TYPE = ARRAY [0..32) OF BOOL; Trits: TYPE = {P, S, F, X}; Pat: TYPE = ARRAY [0..6) OF Trits; XthBitOfN: PUBLIC PROC [x, n: INT] RETURNS [BOOL] = {RETURN [IF x<0 THEN FALSE ELSE (n/BitOps.TwoToThe[x]) MOD 2 =1]}; F: PROC [n, k, i: NAT] RETURNS [BOOL] ~ { in: BOOL = XthBitOfN[n, i]; kn: BOOL = XthBitOfN[n, k]; IF ~in THEN { IF n=0 THEN RETURN [kn] ELSE RETURN [kn OR F[n-1, k, i]]} ELSE { IF n=0 THEN RETURN [FALSE] ELSE RETURN [kn AND F[n-1, k, i]] }; }; RMask: PROC [k: NAT] RETURNS [t: Mask] ~ { FOR i: INT IN [0..32) DO t[i] _ F[5, k, 31-i]; ENDLOOP; }; Pattern: PROC [k: NAT] RETURNS [lowToHi: Pat] ~ { isOne: BOOL _ XthBitOfN[0, k]; lowToHi[0] _ IF isOne THEN X ELSE F; FOR bit: NAT IN [1..6) DO isOne _ XthBitOfN[bit, k]; lowToHi[bit] _ SELECT TRUE FROM isOne AND lowToHi[bit-1]=X => X, isOne => S, ~isOne AND lowToHi[bit-1]=X => F, ~isOne => P, ENDCASE => ERROR; ENDLOOP; }; ApplyPattern: PROC [k, i: NAT] RETURNS [b: BOOL _ FALSE] ~ { lowToHi: Pat _ Pattern[i]; IF lowToHi[0]=F THEN b _ XthBitOfN[0, k]; FOR bit: NAT IN [1..6) DO b _ SELECT lowToHi[bit] FROM X => b, S => b AND XthBitOfN[bit, k], F, P => b OR XthBitOfN[bit, k], ENDCASE => ERROR; ENDLOOP; }; SMask: PROC [k: NAT] RETURNS [t: Mask] ~ { lowToHi: Pat _ Pattern[k]; FOR i: INT IN [0..32) DO t[i] _ ApplyPattern[k, 31-i]; ENDLOOP; }; Check: PROC RETURNS [ok: BOOL _ TRUE, bug: INT _ -1] ~ { Diff: PROC [m1, m2: Mask] RETURNS [BOOL _ FALSE] ~ { FOR i: NAT IN [0..32) DO IF m1[i]#m2[i] THEN RETURN[TRUE]; ENDLOOP; }; FOR k: NAT IN [0..32) DO IF Diff[SMask[k], RMask[k]] THEN RETURN[FALSE, k]; ENDLOOP; }; END. ΖEUProofs.mesa Copyright c 1985 by Xerox Corporation. All rights reserved. Louis Monier June 9, 1986 4:15:41 pm PDT Bertrand Serlet June 9, 1986 0:25:43 am PDT Last Edited by: Louis Monier September 15, 1986 3:43:07 pm PDT Warning: bit 0 is the LOW order bit (lsb) -- Proves the mask generator for the field unit; i is the slice number, k the input -- Recursive construction -- Serial construction, used to make the layout -- The ultimate check Κ#– "cedar" style˜codešœ ™ Kšœ Οmœ1™—K˜KšΟk œ˜K˜•StartOfExpansion[]šΠbnœžœž˜Kšžœ ˜Kšž˜—K˜Kš œžœžœ žœžœ˜#Kšœžœ˜Kšœžœžœžœ˜"K™š Οn œžœžœžœžœžœ˜3Jšœ)™)Jš œžœžœžœžœžœžœ˜B—™SK˜K™š  œžœ žœžœžœ˜)Kšœžœ˜Kšœžœ˜šžœžœ˜ Kšžœžœžœ˜Kšžœžœžœ˜!—šžœ˜Kšžœžœžœžœ˜Kšžœžœžœ˜!Kšœ˜—K˜—š œžœžœžœ˜*šžœžœžœ ž˜Kšœ˜Kšžœ˜—K˜—K˜Kšœ/™/š œžœžœžœ˜1Kšœ˜Kšœ žœžœžœ˜$šžœžœžœž˜Kšœ˜šœžœžœž˜Kšœžœ˜ Kšœ ˜ Kšœžœ˜!Kšœ ˜ Kšžœžœ˜—Kšžœ˜—K˜—š   œžœžœžœžœžœ˜