#include <stdio.h>

void swap(int * p, int * q)
{                        /*@{}&7c @XPC {@CP {*p = a}    @Eq {wedge} @CP {*q =   b}}*/
   *p += *q;        /*@{}&7c @XPC {@CP {*p = a+b} @Eq {wedge} @CP {*q =   b}}*/
   *q -= *p;        /*@{}&7c @XPC {@CP {*p = a+b} @Eq {wedge} @CP {*q = -a}}*/
   *p += *q;        /*@{}&7c @XPC {@CP {*p = b }     @Eq {wedge} @CP {*q = -a}}*/
   *q = 0 - *q;    /*@{}&7c @XPC {@CP {*p = b}     @Eq {wedge} @CP {*q =   a}}*/
}

int main () {
  int i=4, j=7;
  swap( &i, &j );
  printf("i = %d; j = %d\n", i, j);
  return 0;
}