Package: StateInvariantObligation

StateInvariantObligation

nameinstructionbranchcomplexitylinemethod
StateInvariantObligation(AAssignmentStm, IPOContextStack, IPogAssistantFactory)
M: 46 C: 88
66%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 7 C: 20
74%
M: 0 C: 1
100%
StateInvariantObligation(AAtomicStm, IPOContextStack, IPogAssistantFactory)
M: 0 C: 82
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 16
100%
M: 0 C: 1
100%
StateInvariantObligation(AClassInvariantDefinition, IPOContextStack, IPogAssistantFactory)
M: 0 C: 25
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
StateInvariantObligation(AExplicitOperationDefinition, IPOContextStack, IPogAssistantFactory)
M: 25 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 5 C: 0
0%
M: 1 C: 0
0%
StateInvariantObligation(AImplicitOperationDefinition, IPOContextStack, IPogAssistantFactory)
M: 35 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 7 C: 0
0%
M: 1 C: 0
0%
extractInv(AAtomicStm)
M: 19 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 4 C: 0
0%
M: 1 C: 0
0%
getStateName(PDefinition)
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
invDefs(PDefinition)
M: 38 C: 0
0%
M: 4 C: 0
0%
M: 3 C: 0
0%
M: 8 C: 0
0%
M: 1 C: 0
0%
invDefs(SClassDefinition)
M: 0 C: 30
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
makeInvApplyExp(AAtomicStm)
M: 4 C: 87
96%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 1 C: 11
92%
M: 0 C: 1
100%

Coverage

1: /*******************************************************************************
2: *
3: *        Copyright (C) 2008 Fujitsu Services Ltd.
4: *
5: *        Author: Nick Battle
6: *
7: *        This file is part of VDMJ.
8: *
9: *        VDMJ is free software: you can redistribute it and/or modify
10: *        it under the terms of the GNU General Public License as published by
11: *        the Free Software Foundation, either version 3 of the License, or
12: *        (at your option) any later version.
13: *
14: *        VDMJ is distributed in the hope that it will be useful,
15: *        but WITHOUT ANY WARRANTY; without even the implied warranty of
16: *        MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17: *        GNU General Public License for more details.
18: *
19: *        You should have received a copy of the GNU General Public License
20: *        along with VDMJ. If not, see <http://www.gnu.org/licenses/>.
21: *
22: ******************************************************************************/
23:
24: package org.overture.pog.obligation;
25:
26: import java.util.LinkedList;
27: import java.util.List;
28: import java.util.Vector;
29:
30: import org.overture.ast.analysis.AnalysisException;
31: import org.overture.ast.definitions.AClassInvariantDefinition;
32: import org.overture.ast.definitions.AEqualsDefinition;
33: import org.overture.ast.definitions.AExplicitOperationDefinition;
34: import org.overture.ast.definitions.AImplicitOperationDefinition;
35: import org.overture.ast.definitions.AStateDefinition;
36: import org.overture.ast.definitions.PDefinition;
37: import org.overture.ast.definitions.SClassDefinition;
38: import org.overture.ast.expressions.AApplyExp;
39: import org.overture.ast.expressions.ALetDefExp;
40: import org.overture.ast.expressions.AVariableExp;
41: import org.overture.ast.expressions.PExp;
42: import org.overture.ast.factory.AstExpressionFactory;
43: import org.overture.ast.lex.LexNameToken;
44: import org.overture.ast.statements.AAssignmentStm;
45: import org.overture.ast.statements.AAtomicStm;
46: import org.overture.ast.types.ABooleanBasicType;
47: import org.overture.ast.types.AFieldField;
48: import org.overture.pog.pub.IPOContextStack;
49: import org.overture.pog.pub.IPogAssistantFactory;
50: import org.overture.pog.pub.POType;
51: import org.overture.pog.utility.Substitution;
52: import org.overture.pog.visitors.IVariableSubVisitor;
53:
54: public class StateInvariantObligation extends ProofObligation
55: {
56:         private static final long serialVersionUID = -5828298910806421399L;
57:
58:         public final IPogAssistantFactory assistantFactory;
59:
60:         public StateInvariantObligation(AAssignmentStm ass, IPOContextStack ctxt,
61:                         IPogAssistantFactory af) throws AnalysisException
62:         {
63:                 super(ass, POType.STATE_INV, ctxt, ass.getLocation(), af);
64:                 assistantFactory = af;
65:
66:•                if (ass.getClassDefinition() != null)
67:                 {
68:                         PExp old_invs = invDefs(ass.getClassDefinition());
69:
70:                         String hash;
71:                         hash = ass.getTarget().apply(af.getStateDesignatorNameGetter());
72:                         Substitution sub = new Substitution(new LexNameToken("", hash, null), ass.getExp().clone());
73:                         PExp new_invs = old_invs.clone().apply(af.getVarSubVisitor(), sub);
74:
75:                         stitch = AstExpressionFactory.newAImpliesBooleanBinaryExp(old_invs, new_invs);
76:                         valuetree.setPredicate(ctxt.getPredWithContext(stitch));
77:                 } else
78:                 {
79:                         AStateDefinition def = ass.getStateDefinition();
80:                         ALetDefExp letExp = new ALetDefExp();
81:                         letExp.setType(def.getInvExpression().getType().clone());
82:                         List<PDefinition> invDefs = new Vector<PDefinition>();
83:                         AEqualsDefinition local = new AEqualsDefinition();
84:                         local.setExpType(def.getRecordType().clone());
85:                         local.setPattern(def.getInvPattern().clone());
86:                         local.setName(def.getName().clone());
87:                         AVariableExp varExp = getVarExp(def.getName(), def.clone());
88:                         varExp.setType(def.getRecordType().clone());
89:                         local.setTest(varExp);
90:                         invDefs.add(local);
91:                         letExp.setLocalDefs(invDefs);
92:                         letExp.setExpression(def.getInvExpression().clone());
93:
94:                         stitch = letExp;
95:                         valuetree.setPredicate(ctxt.getPredWithContext(stitch));
96:                 }
97:         }
98:
99:         public StateInvariantObligation(AClassInvariantDefinition def,
100:                         IPOContextStack ctxt, IPogAssistantFactory af)
101:                         throws AnalysisException
102:         {
103:                 super(def, POType.STATE_INV_INIT, ctxt, def.getLocation(), af);
104:                 assistantFactory = af;
105:
106:                 // After instance variable initializers
107:
108:                 stitch = invDefs(def.getClassDefinition());
109:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
110:         }
111:
112:         public StateInvariantObligation(AExplicitOperationDefinition def,
113:                         IPOContextStack ctxt, IPogAssistantFactory af)
114:                         throws AnalysisException
115:         {
116:                 super(def, POType.STATE_INV, ctxt, def.getLocation(), af);
117:                 assistantFactory = af;
118:
119:                 // After def.getName() constructor body
120:                 stitch = invDefs(def.getClassDefinition());
121:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
122:         }
123:
124:         public StateInvariantObligation(AAtomicStm atom, IPOContextStack ctxt,
125:                         IPogAssistantFactory af) throws AnalysisException
126:         {
127:                 super(atom, POType.STATE_INV, ctxt, atom.getLocation(), af);
128:                 assistantFactory = af;
129:
130:                 PExp invApplyExp = makeInvApplyExp(atom);
131:
132:                 PExp invApplyExpForSub = invApplyExp.clone();
133:
134:                 List<Substitution> subs = new LinkedList<Substitution>();
135:•                for (AAssignmentStm asgn : atom.getAssignments())
136:                 {
137:                         String hash = asgn.getTarget().apply(af.getStateDesignatorNameGetter());
138:                         subs.add(new Substitution(hash, asgn.getExp().clone()));
139:                 }
140:                 IVariableSubVisitor varSubVisitor = af.getVarSubVisitor();
141:•                for (Substitution sub : subs)
142:                 {
143:                         invApplyExpForSub = invApplyExpForSub.apply(varSubVisitor, sub);
144:                 }
145:
146:                 stitch = AstExpressionFactory.newAImpliesBooleanBinaryExp(invApplyExp, invApplyExpForSub);
147:                 valuetree.setPredicate(stitch);
148:         }
149:
150:         private PExp makeInvApplyExp(AAtomicStm atom)
151:         {
152:                 AStateDefinition stateDef = atom.getAssignments().get(0).getStateDefinition();
153:•                if (stateDef == null)
154:                 {
155:                         return extractInv(atom);
156:                 }
157:                 String stateName = getStateName(stateDef);
158:                 List<PExp> arglist = new Vector<PExp>();
159:•                for (AFieldField f : stateDef.getFields())
160:                 {
161:                         arglist.add(getVarExp(f.getTagname().clone(), stateDef.clone(),f.getType()));
162:                 }
163:                 PExp mkExp = AstExpressionFactory.newAMkTypeExp(new LexNameToken("", stateName, null), stateDef.getRecordType().clone(), arglist);
164:                 AApplyExp invApplyExp = getApplyExp(getVarExp(stateDef.getInvdef().getName().clone(), stateDef.getInvdef().clone(), stateDef.getInvdef().getType().clone()), new ABooleanBasicType(), mkExp);
165:                 invApplyExp.getRoot().setType(stateDef.getInvdef().getType().clone());
166:                 return invApplyExp;
167:         }
168:
169:         private String getStateName(PDefinition stateDef)
170:         {
171:                 return stateDef.getName().getName();
172:         }
173:
174:         private PExp extractInv(AAtomicStm atom)
175:         {
176:                 AAssignmentStm x = atom.getAssignments().get(0);
177:•                if (x.getClassDefinition() != null)
178:                 {
179:                         return invDefs(x.getClassDefinition());
180:                 } else
181:                 {
182:                         return invDefs(x.getStateDefinition());
183:                 }
184:         }
185:
186:         public StateInvariantObligation(AImplicitOperationDefinition def,
187:                         IPOContextStack ctxt, IPogAssistantFactory af)
188:                         throws AnalysisException
189:         {
190:                 super(def, POType.STATE_INV, ctxt, def.getLocation(), af);
191:                 assistantFactory = af;
192:
193:•                if (def.getClassDefinition() == null)
194:                 {
195:                         stitch = invDefs(def.getClassDefinition());
196:                 } else
197:                 {
198:                         stitch = invDefs(def.getStateDefinition());
199:                 }
200:
201:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
202:                 // valuetree.setContext(ctxt.getContextNodeList());
203:         }
204:
205:         private PExp invDefs(SClassDefinition def)
206:         {
207:                 PExp root = null;
208:
209:•                for (PDefinition d : assistantFactory.createSClassDefinitionAssistant().getInvDefs(def.clone()))
210:                 {
211:                         AClassInvariantDefinition cid = (AClassInvariantDefinition) d;
212:                         root = makeAnd(root, cid.getExpression().clone());
213:                 }
214:
215:                 return root;
216:         }
217:
218:         private PExp invDefs(PDefinition def)
219:         {
220:
221:•                if (def instanceof AStateDefinition)
222:                 {
223:                         return ((AStateDefinition) def).getInvdef().getBody();
224:                 } else
225:                 {
226:
227:                         PExp root = null;
228:
229:•                        for (PDefinition d : assistantFactory.createSClassDefinitionAssistant().getInvDefs((SClassDefinition) def))
230:                         {
231:                                 AClassInvariantDefinition cid = (AClassInvariantDefinition) d;
232:                                 root = makeAnd(root, cid.getExpression().clone());
233:                         }
234:
235:                         return root;
236:                 }
237:         }
238:
239: }