specification SPROT_service [PUT,GET] :noexit

  behaviour

    SERVICE [PUT,GET]

where

   process SERVICE [PUT,GET] :noexit :=
     PUT; GET;
       SERVICE [PUT,GET]
   endproc

endspec