Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/examples/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 646 B image not shown  

Quelle  checker_example.pvs   Sprache: 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

98%


¤ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.