|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
closest_approach_3D.prf
Sprache: Lisp
Untersuchung PVS©
|
|
|
(function_image_extra
(image_singleton 0
(image_singleton-1 nil 3318609248 ("" (grind-with-ext) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(R formal-type-decl nil function_image_extra nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(finite_image application-judgement "finite_set[R]"
function_image_aux nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(singleton? const-decl "bool" sets nil)
(image const-decl "set[R]" function_image nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(D formal-type-decl nil function_image_extra nil)
(singleton const-decl "(singleton?)" sets nil))
shostak))
(image_add 0
(image_add-1 nil 3318609300
("" (skolem!)
(("" (rewrite "add_as_union")
(("" (rewrite "add_as_union")
(("" (rewrite "image_union")
(("" (rewrite "image_singleton") nil nil)) nil))
nil))
nil))
nil)
((add_as_union formula-decl nil sets_lemmas nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(D formal-type-decl nil function_image_extra nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(nonempty_union2 application-judgement "(nonempty?)" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(image_union formula-decl nil function_image nil)
(finite_image application-judgement "finite_set[R]"
function_image_aux nil)
(image_singleton formula-decl nil function_image_extra nil)
(R formal-type-decl nil function_image_extra nil)
(image const-decl "set[R]" function_image nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.23Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
|
|
|
|
|
