Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: PVS

Columbo aufrufen.summary zum Wurzelverzeichnis wechselnMT940 {MT940[547] Hlasm[2002] Haskell[2385]}Datei anzeigen

***
*** top (18:55:8 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
*** Trusted Oracles
***   MetiTarski: MetiTarski Theorem Prover via PVS proof rule metit
***
Proof summary for theory top
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

Proof summary for theory examples
    simple................................proved - complete   [shostak](0.07 s)
    simple_abs............................proved - complete   [shostak](0.05 s)
    sqrtx3_TCC1...........................proved - complete   [shostak](0.02 s)
    sqrtx3................................proved - complete   [shostak](0.02 s)
    tr_35_TCC1............................proved - complete   [shostak](0.01 s)
    tr_35.................................proved - complete   [shostak](0.11 s)
    tr_35_le_TCC1.........................proved - complete   [shostak](0.00 s)
    tr_35_le..............................proved - complete   [shostak](0.01 s)
    sqrt23................................proved - complete   [shostak](0.02 s)
    sin6sqrt2.............................proved - complete   [shostak](0.01 s)
    G_TCC1................................proved - complete   [shostak](0.00 s)
    A_and_S...............................proved - complete   [shostak](0.01 s)
    r_TCC1................................proved - complete   [shostak](0.01 s)
    r_TCC2................................proved - complete   [shostak](0.01 s)
    atan_implementation...................proved - complete   [shostak](0.01 s)
    ajn...................................proved - complete   [shostak](0.01 s)
    ex1_ba_TCC1...........................proved - complete   [shostak](0.01 s)
    ex1_ba_TCC2...........................proved - complete   [shostak](0.04 s)
    ex1_ba................................proved - complete   [shostak](0.01 s)
    ex2_ba_TCC1...........................proved - complete   [shostak](0.02 s)
    ex2_ba................................proved - complete   [shostak](0.02 s)
    ex3_ba_TCC1...........................proved - complete   [shostak](0.02 s)
    ex3_ba................................proved - complete   [shostak](0.01 s)
    ex4_ba................................proved - complete   [shostak](0.01 s)
    ex5_ba_TCC1...........................proved - complete   [shostak](0.05 s)
    ex5_ba................................proved - complete   [shostak](0.01 s)
    ex6_ba................................proved - complete   [shostak](0.01 s)
    ex7_ba................................proved - complete   [shostak](0.01 s)
    quadratic.............................proved - complete   [shostak](0.01 s)
    Tunnel_3_IL...........................proved - complete   [shostak](0.01 s)
    Tunnel_3_IL_LU........................proved - complete   [shostak](0.01 s)
    Ayad_Marche...........................proved - complete   [shostak](0.01 s)
    Theory totals: 32 formulas, 32 attempted, 32 succeeded (0.63 s)

Proof summary for theory Disable
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

Grand Totals: 32 proofs, 32 attempted, 32 succeeded (0.63 s)

[ Original von:0.509Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt. ]