% @(#)$Id: bitwise.lsl,v 1.2 1994/10/08 20:40:25 leavens Exp $
% bitwise operations on numbers,
% with enough slack to accomodate different representations of numbers

bitwise(N): trait
  includes Integer(N), String(Bool, BoolString, int for Int)
  introduces
    NUM_BITS: -> int
    legalbit: int -> Bool
    toBits: N -> BoolString
    fromBits: BoolString -> N
    string_and, string_xor, string_or: BoolString, BoolString -> BoolString
    string_not: BoolString -> BoolString
    bitwise_and, bitwise_xor, bitwise_or: N, N -> N
    bitwise_not: N -> N
  asserts \forall n,n1,n2: N, i: int, bs,bs1,bs2: BoolString
    len(toBits(n)) == NUM_BITS;
    legalbit(i) == (0 <= i) /\ (i < NUM_BITS);
    fromBits(toBits(n)) == n;
    legalbit(i) => (toBits(0))[i] == false;

    len(string_not(bs)) == NUM_BITS;
    len(string_and(bs1,bs2)) == NUM_BITS;
    len(string_xor(bs1,bs2)) == NUM_BITS;
    len(string_or(bs1,bs2)) == NUM_BITS;

    legalbit(i) => ((string_not(bs))[i] = ~(bs[i]));
    legalbit(i) => ((string_and(bs1,bs2))[i] = (bs1[i]) /\ (bs2[i]));
    legalbit(i) => ((string_or(bs1,bs2))[i] = (bs1[i]) \/ (bs2[i]));
    legalbit(i) => ((string_xor(bs1,bs2))[i] = ~((bs1[i]) = (bs2[i])));

    bitwise_not(n) == fromBits(string_not(toBits(n)));
    bitwise_and(n1,n2) == fromBits(string_and(toBits(n1), toBits(n2)));
    bitwise_or(n1,n2) == fromBits(string_or(toBits(n1), toBits(n2)));
    bitwise_xor(n1,n2) == fromBits(string_xor(toBits(n1), toBits(n2)));

[Index]

HTML generated using lcpp2html.