Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Fortran/f90gl-1.2.15/examples/F/   (NIST Fortran ©)  Datei vom 26.0.2004 mit Größe 36 kB image not shown  

SSL 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.12 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.

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.