Computer-Aided Program Development Institute of Computer Science Faculty of Engineering, Christian-Albrechts-University of Kiel

{***********************************************************************}
{* 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