specification exa4_1[a,b] : exit

  behaviour

    a; b; exit

endspec