Bitwise Swap

This shows basic use of SPARK modular types (the unsigned of C/C++) with bitwise operators, and a contract relating input and output values of a procedure. In the initial version, the postcondition cannot be proved because a xor operation is missing. And yes, 3 xor equal a swap!