specification(Z=f(X),
   while(more,((
     Z=X,
     (
	 (X->(
	     repeat((skip&(Z=X,empty)),until,not(X)) &
	     repeat((skip&(Z=not(X),empty)),until,not(X))))
         ,
         (not(X)->(
	     repeat((skip&(Z=not(X),empty)),until,not(X))))
     )
    & skip
    )))
).

implementation(Z=f(X),
    exists(y,(
    not(y),
    [](
           (
	   next(y) = ((not(X),not(y));(X,y)),
	   Z = ((X,not(y);(not(X),y)))
           )
      )
    ))
).

?- specification(z=f(x),Y),ex((trace(x,[1,1,0,1,1,1,0,0,1,0,1]),Y)).

?- speficication(z=f(x),S),implementation(z=f(x),I),
   ex(I->fin_free(S)).