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 {$0 == -10} -> STOP | return {$0 == 25} -> STOP ).
Spec2 = ( return {$0 == 7} -> STOP ).