// @(#)$Header: /home/larch/research/master/larch/lc++/samples/cpp_types/short.lh,v 1.21 1998/08/27 22:56:47 leavens Exp $
// Larch/C++ specification of C++'s short int type

// The following uses clause is implicit in Larch/C++.
// You don't have to write it; it's included as an example of the Larch/C++
// implicit use of traits for C++ built-in types.
/*
   uses short, MutableObj(short);
*/

//@ invariant \A i: Obj[short] (inRange(i\any));


// ********************************************************
// arithmetic operations: +, -, *, /, and %
// ********************************************************

short operator + (short i, short j);
//@ behavior {
//@   requires inRange(i + j);
//@   ensures  returns => result = i + j;
//@ }

short operator - (short i, short j);
//@ behavior {
//@   requires inRange(i - j);
//@   ensures  returns => result = i - j;
//@ }

short operator - (short i);
//@ behavior { // unary - operation
//@   requires inRange(-i);
//@   ensures  returns => result = -i;
//@ }

short operator + (short i);
//@ behavior { // unary + operation
//@   ensures  returns => result = i;
//@ }

short operator * (short i, short j);
//@ behavior {
//@   requires inRange(i * j);
//@   ensures  returns => result = i * j;
//@ }

// operator / and operator % are intentionally underspecified;
// see the C++ reference manual (section 5.6) for the reasons.

short operator / (short i, short j);
//@ behavior {
//@   requires (((j > 0) /\ (i >= 0)) \/ ((j < 0) /\ (i < 0)))  // same sign
//@ 	     /\ inRange(div(abs(i), abs(j)));
//@   ensures  returns => result = div(abs(i),abs(j));
//@ also
//@   requires (((j > 0) /\ (i < 0)) \/ ((j < 0) /\ (i >= 0)))// different sign
//@            /\ inRange((-div(abs(i), abs(j))) - 1);
//@   ensures  returns =>
//@              (result = -div(abs(i), abs(j))
//@               \/ result = (-div(abs(i), abs(j))) - 1);
//@ }

short operator % (short i, short j);
//@ behavior {
//@   requires (((j > 0) /\ (i >= 0)) \/ ((j < 0) /\ (i < 0)))  // same sign
//@ 	     /\ inRange(mod(abs(i), abs(j)));
//@   ensures  returns => result = mod(i,j);
//@ also
//@   requires (((j > 0) /\ (i < 0)) \/ ((j < 0) /\ (i >= 0)))// different sign
//@            /\ inRange(-mod(abs(i), abs(j)))
//@            /\ inRange(abs(j) - mod(abs(i), abs(j)));
//@   ensures  returns =>
//@             (result = -mod(abs(i), abs(j))
//@              \/ result = abs(j) - mod(abs(i), abs(j)));
//@ }

// ********************************************************
// equality operators: == and  !=
// ********************************************************

bool operator == (short i, short j);
//@ behavior {
//@   ensures returns => result = (i = j);
//@ }

bool operator != (short i, short j);
//@ behavior {
//@   ensures returns => result = (i ~= j);
//@ }


// ********************************************************
// relational operators: <, >, <=, and >= 
// ********************************************************

bool operator < (short i, short j);
//@ behavior {
//@   ensures returns => result = (i < j);
//@ }

bool operator > (short i, short j);
//@ behavior {
//@   ensures returns => result = (i > j);
//@ }

bool operator <= (short i, short j);
//@ behavior {
//@   ensures returns => result = (i <= j);
//@ }

bool operator >= (short i, short j);
//@ behavior {
//@   ensures returns => result = (i >= j);
//@ }


// ********************************************************
// logical operators: !, &&, and ||
// ********************************************************

bool operator ! (short i);
//@ behavior {
//@   ensures  returns => result = (i = 0);
//@ }    

bool operator && (short i, short j);
//@ behavior {
//@   ensures  returns => result = ((i ~= 0) /\ (j ~= 0));
//@ }    

bool operator || (short i, short j);
//@ behavior {
//@   ensures  returns => result = ((i ~= 0) \/ (j ~= 0));
//@ }    


// ********************************************************
// increment/decrement operators: ++ and --
// ********************************************************

short& operator ++ (short& i);
//@ behavior {  // prefix ++; e.g. ++i
//@   requires assigned(i, pre) /\ inRange(i^ + 1);
//@   modifies i;
//@   ensures  returns => result = i /\ i' = i^ + 1;
//@   ensures redundantly  returns => assigned(result, post);
//@ }    

short operator ++ (short& i, int);
//@ behavior {  // postfix ++; e.g. i++
//@   requires assigned(i, pre) /\ inRange(i^ + 1);
//@   modifies i;
//@   ensures  returns => result = i^ /\ i' = i^ + 1;
//@ }    

short& operator -- (short& i);
//@ behavior {  // prefix --; e.g. --i
//@   requires assigned(i, pre) /\ inRange(i^ - 1);
//@   modifies i;
//@   ensures  returns => result = i /\ i' = i^ - 1;
//@   ensures redundantly  returns => assigned(result, post);
//@ }    

short operator -- (short& i, int);
//@ behavior {  // postfix --; e.g. i--
//@   requires assigned(i, pre) /\ inRange(i^ - 1);
//@   modifies i;
//@   ensures  returns => result = i^ /\ i' = i^ - 1;
//@ }    


// ********************************************************
// assignment operators: =, +=, -=, *=, /=, and  %=
// ********************************************************
short& operator = (short& i, short j);
//@ behavior {
//@   requires assigned(i, pre);
//@   modifies i;
//@   ensures  returns => (result = i /\ i' = j);
//@   ensures redundantly  returns => assigned(result, post);
//@ }    

short& operator += (short& i, short j);
//@ behavior {
//@   requires assigned(i, pre) /\ inRange(i^ + j);
//@   modifies i;
//@   ensures  returns => (result = i /\ i' = i^ + j);
//@   ensures redundantly  returns => assigned(result, post);
//@ }    

short& operator -= (short& i, short j);
//@ behavior {
//@   requires assigned(i, pre) /\ inRange(i^ - j);
//@   modifies i;
//@   ensures  returns => (result = i /\ i' = i^ - j);
//@   ensures redundantly  returns => assigned(result, post);
//@ }    

short& operator *= (short& i, short j);
//@ behavior {
//@   requires assigned(i, pre) /\ inRange(i^ * j);
//@   modifies i;
//@   ensures  returns => (result = i /\ i' = i^ * j);
//@   ensures redundantly  returns => assigned(result, post);
//@ }    

short& operator /= (short& i, short j);
//@ behavior {
//@   requires assigned(i, pre);
//@   {
//@     requires (((j > 0) /\ (i^ >= 0)) \/ ((j < 0) /\ (i^ < 0))) // same sign
//@ 	       /\ inRange(div(abs(i^), abs(j)));
//@     modifies i;
//@     ensures  returns => (result = i /\ i' = div(abs(i^), abs(j)));
//@
//@   also
//@
//@     requires (((j > 0) /\ (i^ < 0)) \/ ((j < 0) /\ (i^ >= 0))) // diff sign
//@              /\ inRange((-div(abs(i^), abs(j))) - 1);
//@     modifies i;
//@     ensures  returns =>
//@                (result = i
//@                    /\ (i' = -div(abs(i^), abs(j)
//@                        \/ i' = (-div(abs(i^), abs(j))) - 1)));
//@   }
//@   ensures redundantly returns => assigned(result, post);
//@ }    

short& operator %= (short& i, short j);
//@ behavior {
//@   requires assigned(i, pre);
//@   {
//@     requires (((j > 0) /\ (i^ >= 0)) \/ ((j < 0) /\ (i^ < 0)))  // same sign
//@ 	       /\ inRange(mod(abs(i^), abs(j)));
//@     modifies i;
//@     ensures  returns => (result = i /\ i' = mod(i^,j));
//@
//@   also
//@     requires (((j > 0) /\ (i^ < 0)) \/ ((j < 0) /\ (i^ >= 0))) // diff sign
//@         /\ inRange(-mod(abs(i^), abs(j)))
//@         /\ inRange(abs(j) - mod(abs(i^), abs(j)));
//@     modifies i;
//@     ensures  returns =>
//@                (result = i /\ i' = -mod(abs(i^), abs(j))
//@                 \/ i' = abs(j) - mod(abs(i^), abs(j)));
//@   }
//@   ensures redundantly returns => assigned(result, post);
//@ }    


// ********************************************************
// bitwise logical operators
// ********************************************************

//@ uses bitwise(short for N);

short operator & (short i, short j);
//@ behavior {
//@   ensures returns => result = bitwise_and(i,j);
//@ }

short operator ^ (short i, short j);
//@ behavior {
//@   ensures returns => result = bitwise_xor(i,j);
//@ }

short operator | (short i, short j);
//@ behavior {
//@   ensures returns => result = bitwise_or(i,j);
//@ }

short operator ~ (short i);
//@ behavior {
//@   ensures returns => result = bitwise_not(i);
//@ }

[Index]

HTML generated using lcpp2html.