Quelle  checker_example.pvs

% Naive primality test
is_prime : THEORY
BEGIN

  is_prime?(n:nat) : bool =
    n > 1 AND (n = 2 OR FORALL (j:subrange(2,n-1)) : mod(n,j) /= 0)

END is_prime

checker_example : THEORY
BEGIN
 
  IMPORTING PVSioChecker@pvsio_checker,
            is_prime

  check?(fin:IStream,fout:OStream) : bool = 
    LET n  = str2pvs[nat](readln_checker(fin)),  % Read n from file
        io = str2pvs[bool](readln_checker(fin)), % Read output from file
        pvs = is_prime?(n) IN
      check_bool(fout,"",pvs,io) % Check PVS output against ouput in file       

  main(file:string,records:nat): void =
    checker(file,check?,records)

END checker_example