products/Sources/formale Sprachen/Isabelle/HOL/Mirabelle/Tools/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: SML

Original von: Isabelle©
(*  Title:      HOL/Mirabelle/Tools/mirabelle_refute.ML
    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
*)

structure Mirabelle_Refute : MIRABELLE_ACTION =
struct


(* FIXME:
fun refute_action args timeout {pre=st, ...} = 
  let
    val subgoal = 1
    val thy = Proof.theory_of st
    val thm = #goal (Proof.raw_goal st)

    val refute = Refute.refute_goal thy args thm
    val _ = Timeout.apply timeout refute subgoal
  in
    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))

    val r =
      if Substring.isSubstring "model found" writ_log
      then
        if Substring.isSubstring "spurious" warn_log
        then SOME "potential counterexample"
        else SOME "real counterexample (bug?)"
      else
        if Substring.isSubstring "time limit" writ_log
        then SOME "no counterexample (timeout)"
        else if Substring.isSubstring "Search terminated" writ_log
        then SOME "no counterexample (normal termination)"
        else SOME "no counterexample (unknown)"
  in r end
*)

fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*)

end

¤ Dauer der Verarbeitung: 0.9 Sekunden  (vorverarbeitet)  ¤



zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
sprechenden Kalenders

Eigene Datei ansehen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff