Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: yts803.cob   Sprache: SML

Original von: Isabelle©

(*  Title:      HOL/Tools/SMT/smt_failure.ML
    Author:     Sascha Boehme, TU Muenchen

Failures and exception of SMT.
*)


signature SMT_FAILURE =
sig
  datatype failure =
    Counterexample of bool |
    Time_Out |
    Out_Of_Memory |
    Abnormal_Termination of int |
    Other_Failure of string
  val string_of_failure: failure -> string
  exception SMT of failure
end;

structure SMT_Failure: SMT_FAILURE =
struct

datatype failure =
  Counterexample of bool |
  Time_Out |
  Out_Of_Memory |
  Abnormal_Termination of int |
  Other_Failure of string

fun string_of_failure (Counterexample genuine) =
      if genuine then "Counterexample found (possibly spurious)"
      else "Potential counterexample found"
  | string_of_failure Time_Out = "Timed out"
  | string_of_failure Out_Of_Memory = "Ran out of memory"
  | string_of_failure (Abnormal_Termination err) =
      "Solver terminated abnormally with error code " ^ string_of_int err
  | string_of_failure (Other_Failure msg) = msg

exception SMT of failure

end;

¤ Dauer der Verarbeitung: 0.18 Sekunden  (vorverarbeitet)  ¤





Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik