is_prime?(n:nat) : bool =
n > 1 AND (n = 2 ORFORALL (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
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.
