git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7793 3260e6d1-4efc-4170-b0a7-36055960796d

su4sml/src/wfcpog/test-data.sml

@@ -78,15 +78,22 @@ val md7 = rename_wfpo "md7" (TAX_Data.put ({key=9,max_depth=7}) tax)
 val md8 = rename_wfpo "md8" (TAX_Data.put ({key=9,max_depth=8}) tax)
 *)
 
-(*  
-val wfs = [inf,vis,md0,md1,md2,md3,md4,md5,md6,md7,md8,rfm_SC_wfc]
-val pos = [lsk,cm,sm,om,cmd,quy]
+(* 
+val wfs = [wfc_inf,wfc_vis]
+val pos = [po_lsk,po_cm,po_sm,po_cmd,po_quy]
+*)
+
+
+val wfs = [wfc_rfm_SC]
+val pos = [po_rfm_SC]
+
+
+(* 
+val wfs = []
+val pos = [po_cm,po_sm]
 *)
 
 (* 
-val wfs = [rfm_SC_wfc]
-val pos = [rfm_SC_pog]
-*)
-
 val wfs = []
-val pos = [po_cm,po_sm]
+val pos = [po_cstr]
+*)

su4sml/src/wfcpog/visibility_consistency.sml

@@ -42,6 +42,8 @@
 (** Implementation of the Liskov Substitiution Principle. *)
 signature WFCPOG_VISIBILITY_CONSTRAINT =
 sig
+    (** Checks if the pre- and postconditions of a given operation just
+      * access public classes/operations/attributes. *)
     val are_conditions_visible : WFCPOG.wfpo -> Rep.Model -> bool
 end
 structure WFCPOG_Visibility_Constraint:WFCPOG_VISIBILITY_CONSTRAINT = 

su4sml/src/wfcpog/wfcpog_registry.sml

@@ -85,6 +85,8 @@ sig
 							 
     (** Execute a wfc.*)    
     val check_wfc          : Rep.Model -> WFCPOG.wfpo -> bool
+    (** Execute a wfc with verbose output in case of a false wfc. *)
+    (* val check_wfc_verbose  : Rep.Model -> WFCPOG.wfpo -> bool *)
     (** Execute a list of wfcs.*)
     val check_wfcs         : Rep.Model -> WFCPOG.wfpo list -> bool
 
@@ -183,7 +185,7 @@ val supported_wfs = [
      name            = "WFC Interface Consistency (complete)",
      description     = "Checking of two subconstraints: \n wfc_inf_ster: Checks if all operations of an interface don't have the stereotypes 'create' or 'destroy'. \n wfc_inf_name : Checks for classes inheriting from more than one interface that there are no nameclashes.\n",
      recommended     = true,
-     depends         = ["inf_ster"],
+     depends         = ["wfc_inf_ster"],
      recommends      = [],
      apply           = WFCPOG.WFC(WFCPOG_Interface_Constraint.is_nameclash_free),
      data            = Datatab.empty
@@ -268,7 +270,7 @@ val supported_pos = [
      name            = "OO Refinement",
      description     = "Generate Proof Obligations for OO data refinement",
      recommended     = true,
-     depends         = [],
+     depends         = ["wfc_rfm"],
      recommends      = [],
      apply           = WFCPOG.POG(WFCPOG_Refine_Constraint.generate_pos),
      data            = Datatab.empty
@@ -338,7 +340,7 @@ val supported_pos = [
      name            = "WFC Constructor Consistency (complete)",
      description     = "Checks two subconstraints: \n cstr_post : Checks if after the execution of any constructor operation all the attributes are initialized.\n cstr_attr: Checks if after the execution of any constructor operation all the attributes are initialized.\n",
      recommended     = false,
-     depends         = ["cstr_post"],
+     depends         = ["po_cstr_post"],
      recommends      = [],
      apply           = WFCPOG.POG(WFCPOG_Constructor_Constraint.attributes_are_inited),
      data            = Datatab.empty
@@ -372,25 +374,38 @@ fun is_pog (WFCPOG.WFPO wfpo) = case #apply wfpo of
 fun process_depends [] model acc = acc 
   | process_depends (h::tail) model  acc =
     let
+	val _ = trace function_calls ("WFCPOG_Registry.process_depends\n")
 	val wfpo  = get_wfpo supported h
+	val _ = trace wgen ("Dependent wfpo " ^ (name_of wfpo) ^ " found.\n")
+	val res = 
+	    case (WFCPOG.apply_of wfpo) of
+		WFCPOG.WFC(a) => (process_depends tail model ((#1 acc)@[a wfpo model],(#2 acc)))
+	      | WFCPOG.POG(a) => (process_depends tail model ((#1 acc),(#2 acc)@(a wfpo model)))
+	val _ = trace function_ends ("WFCPOG_Registry.process_depends\n")
     in
-	case (WFCPOG.apply_of wfpo) of
-	    WFCPOG.WFC(a) => (process_depends tail model ((#1 acc)@[a wfpo model],(#2 acc)))
-	  | WFCPOG.POG(a) => (process_depends tail model ((#1 acc),(#2 acc)@(a wfpo model)))
+	res
     end
 
 
 fun check_wfc model (wfc_sel as WFCPOG.WFPO{identifier,name,description,recommended,depends,recommends,apply,data}:WFCPOG.wfpo)  = 
     let 
 	val _ = trace function_calls ("WFCPOG_Registry.check_wfc\n")
-	val _ = trace wgen (name_of wfc_sel ^ "..............")
+	val _ = trace wgen (name_of wfc_sel ^ ".............." ^ "\n")
 	val res = 
 	    case WFCPOG.apply_of wfc_sel of
 		WFCPOG.WFC(a) => if (depends = []) 
-				 then a wfc_sel model
+				 then 
+				     let 
+					 val _ = trace wgen ("No dependent wfpos.\n")
+				     in
+					 a wfc_sel model
+				     end
 				 else 
 				     let
+					 val _ = trace wgen ("Dependent wfpos detected.\n")
+					 val _ = trace wgen ("Process dependencies ...\n")
 					 val (wfs,pos) = process_depends depends model ([],[])
+					 val _ = trace wgen ("Dependencies processed ...\n")
 				     in
 					 (List.all (fn a => a = true) wfs)
 				     end
@@ -399,6 +414,7 @@ fun check_wfc model (wfc_sel as WFCPOG.WFPO{identifier,name,description,recommen
     in
 	res
     end
+
     
 fun check_wfcs model wfcs = List.all (fn v => (v = true)) (map (check_wfc model) wfcs)