|
% 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
¤ Dauer der Verarbeitung: 0.38 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
