[an error occurred while processing this directive]
{***********************************************************************} {* TEST OF A NUMBER TO BE PRIME *} {***********************************************************************} type DIV basedon NAT, BOOL func divides : (Nat,Nat)Bool axioms all (a, n : Nat) {1} n = 0 => divides(a,n) -> true, {2} lt(0,n) = true & lt(n,a) = true => divides(a,n) -> false, {3} le(a,n) = true => divides(a,n) -> divides(a,sub(n,a)) endoftype type ISPRIM basedon DIV, NAT, BOOL func isp : (Nat)Bool, aux : (Nat,Nat)Bool axioms all (x, a : Nat) {3} isp(x) -> and(ge(x,2),aux(x,2)), {4} le(x,a) = true => aux(x,a) -> true, {5} lt(a,x) = true => aux(x,a) -> and(not(divides(a,x)),aux(x,succ(a))) endoftype {***********************************************************************} {* SOME EXAMPLE TASKS *} {***********************************************************************} task T1 basedon DIV, NAT, BOOL unknown x : Nat goals divides(x,20) = true endoftask task T2 basedon ISPRIM, NAT, BOOL unknown x : Nat goals isp(x) = false endoftask task T3 basedon ISPRIM, NAT, BOOL unknown x : Nat goals isp(x) = true endoftask task T4 basedon ISPRIM, NAT, BOOL unknown x, y : Nat goals isp(x) = true, isp(y) = true, y = succ(succ(x)) endoftask[an error occurred while processing this directive] 31-Jul-2012, 14:17:23 CEST