subconstraint conjugate invariant added

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

su4sml/src/wfcpog/liskov_constraint.sml

@@ -190,13 +190,15 @@ fun strengthen_postcondition wfpo (model as (clist,alist)) =
 	strengthen_postcondition_help cl model
     end
 
+
+
+
 fun conjugate_invariants_help [] model = []
   | conjugate_invariants_help (class::clist) model = 
     let
 	(* get the invariants of all parents *)
-	val invariants = all_invariants_of class model
-	val c_name = string_of_path (name_of class)
- 	val invs = List.map (fn (a,b) => (Predicate(b,type_of_term b,name_of_inv class,[selfarg (type_of class)]))) invariants 
+        val parents = parents_of class model
+ 	val invs = List.map (fn a => Predicate(Variable(varcounter.nextStr(),Rep_Core.type_of a),Rep_Core.type_of a,name_of_inv a,[selfarg (Rep_Core.type_of a)])) parents 
     in
 	if (List.length(invs) = 0)
 	then (conjugate_invariants_help clist model)
@@ -208,10 +210,8 @@ fun conjugate_invariants_help [] model = []
 fun conjugate_invariants wfpo (model as (clist,alist)) = 
     let 
 	val cl = removeOclLibrary clist
-	
     in
 	conjugate_invariants_help cl model
     end
 
 end
-

su4sml/src/wfcpog/test-data.sml

@@ -112,4 +112,4 @@ val wfs = [wfc_vis]
 val pos = []
 *)
 val wfs = []
-val pos = [po_om]
+val pos = [po_lsk]