variables  a,b,c,d ; 

    initialcondition  ((not(a) /\ b) /\ (c /\ d)) ;

    finalcondition  not(b) ;

    begin 
   
     a := b  ; 

     c := (d \/ b) ; 

     if c then begin 

                  b := (a -> c) ; 

                  c := b 

                end 

          else c := a 

    end