forked from Isabelle_DOF/Isabelle_DOF
debugged merge
This commit is contained in:
parent
ba7bd6dc03
commit
0cc010cecc
|
@ -521,15 +521,13 @@ datatype vnt_technique =
|
|||
|
||||
type_synonym verification_and_testing_technique = vnt_technique
|
||||
|
||||
(* modelling exampe of a table ... *)
|
||||
(* modelling example of a table ... *)
|
||||
|
||||
datatype recommandation_level = M | R | HR
|
||||
|
||||
fun table_A_5 :: "vnt_technique \<Rightarrow> sil \<Rightarrow> recommandation_level option"
|
||||
fun table_A_5 :: "vnt_technique \<Rightarrow> sil \<Rightarrow> normative_level option"
|
||||
where "table_A_5 (formal_proof _) = Map.empty( SIL1 \<mapsto> R, SIL2 \<mapsto> R, SIL3 \<mapsto> HR,SIL4 \<mapsto> HR)"
|
||||
|"table_A_5 stat_analysis = Map.empty(SIL0 \<mapsto> R,SIL1 \<mapsto> HR,SIL2 \<mapsto> HR,SIL3 \<mapsto> HR,SIL4 \<mapsto> HR)"
|
||||
|"table_A_5 (dyn_analysis _) = Map.empty(SIL0 \<mapsto> R,SIL1 \<mapsto> HR,SIL2 \<mapsto> HR,SIL3 \<mapsto> HR,SIL4 \<mapsto> HR)"
|
||||
|"table_A_5 metrics = Map.empty( SIL1 \<mapsto> R, SIL2 \<mapsto> R ,SIL3 \<mapsto> R ,SIL4 \<mapsto> R )"
|
||||
|"table_A_5 stat_analysis = Map.empty( SIL1 \<mapsto> HR,SIL2 \<mapsto> HR,SIL3 \<mapsto> HR,SIL4 \<mapsto> HR)"
|
||||
|"table_A_5 (dyn_analysis _) = Map.empty( SIL1 \<mapsto> HR,SIL2 \<mapsto> HR,SIL3 \<mapsto> HR,SIL4 \<mapsto> HR)"
|
||||
|"table_A_5 traceability = Map.empty(SIL0 \<mapsto> R,SIL1 \<mapsto> HR,SIL2 \<mapsto> HR,SIL3 \<mapsto> M ,SIL4 \<mapsto> M )"
|
||||
|
||||
text\<open>The objective of software verification is to examine and arrive at a \<^emph>\<open>judgement\<close> based on
|
||||
\<^emph>\<open>evidence\<close> that output items (process, documentation, software or application) of a specific
|
||||
|
|
Reference in New Issue