cprog prog = my_proc { abstract abs_1,{1},Spec1; } cproc my_proc { predicate (x < 10),(y > 20); } cproc foo { abstract {abs_1,1,Spec2}; } Spec1 = ( return {-10} -> STOP | return {25} -> STOP ). Spec2 = ( return {7} -> STOP ).