| products/sources/formale Sprachen/PVS/trig_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispUntersuchung PVS© |
|
||||||
|
(jatan2
(jatan2_TCC1 0 (jatan2_TCC1-1 nil 3422010249 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil)) nil)) (jatan2_TCC2 0 (jatan2_TCC2-1 nil 3422016445 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil)) nil)) (t1 0 (t1-1 nil 3422010263 ("" (expand "jatan2") (("" (rewrite "atan2_11") nil nil)) nil) ((atan2_11 formula-decl nil atan2_props nil) (jatan2 const-decl "real" jatan2 nil)) shostak)) (t2 0 (t2-1 nil 3422011234 ("" (expand "jatan2") (("" (rewrite "atan2_1m1") (("" (assert) nil nil)) nil)) nil) ((atan2_1m1 formula-decl nil atan2_props nil) (nil application-judgement "nnreal_lt_2pi" atan2 nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (jatan2 const-decl "real" jatan2 nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) nil)) (t3 0 (t3-1 nil 3422016836 ("" (expand "jatan2") (("" (rewrite "atan2_m11") nil nil)) nil) ((atan2_m11 formula-decl nil atan2_props nil) (jatan2 const-decl "real" jatan2 nil)) shostak)) (t4 0 (t4-1 nil 3422016851 ("" (expand "jatan2") (("" (rewrite "atan2_m1m1") (("" (assert) nil nil)) nil)) nil) ((atan2_m1m1 formula-decl nil atan2_props nil) (nil application-judgement "nnreal_lt_2pi" atan2 nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (jatan2 const-decl "real" jatan2 nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) shostak))) ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.34Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
