Package: BinaryExpressionEvaluator

BinaryExpressionEvaluator

nameinstructionbranchcomplexitylinemethod
BinaryExpressionEvaluator()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
addExact(long, long, Context)
M: 8 C: 4
33%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 2 C: 1
33%
M: 0 C: 1
100%
caseAAndBooleanBinaryExp(AAndBooleanBinaryExp, Context)
M: 8 C: 43
84%
M: 2 C: 6
75%
M: 2 C: 3
60%
M: 3 C: 11
79%
M: 0 C: 1
100%
caseACompBinaryExp(ACompBinaryExp, Context)
M: 30 C: 87
74%
M: 4 C: 6
60%
M: 3 C: 3
50%
M: 6 C: 20
77%
M: 0 C: 1
100%
caseADivNumericBinaryExp(ADivNumericBinaryExp, Context)
M: 13 C: 33
72%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 3 C: 5
63%
M: 0 C: 1
100%
caseADivideNumericBinaryExp(ADivideNumericBinaryExp, Context)
M: 6 C: 27
82%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 2 C: 4
67%
M: 0 C: 1
100%
caseADomainResByBinaryExp(ADomainResByBinaryExp, Context)
M: 6 C: 51
89%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 2 C: 9
82%
M: 0 C: 1
100%
caseADomainResToBinaryExp(ADomainResToBinaryExp, Context)
M: 6 C: 51
89%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 2 C: 9
82%
M: 0 C: 1
100%
caseAEqualsBinaryExp(AEqualsBinaryExp, Context)
M: 2 C: 32
94%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 1 C: 7
88%
M: 0 C: 1
100%
caseAEquivalentBooleanBinaryExp(AEquivalentBooleanBinaryExp, Context)
M: 10 C: 37
79%
M: 2 C: 4
67%
M: 2 C: 2
50%
M: 3 C: 5
63%
M: 0 C: 1
100%
caseAGreaterEqualNumericBinaryExp(AGreaterEqualNumericBinaryExp, Context)
M: 18 C: 39
68%
M: 3 C: 5
63%
M: 3 C: 2
40%
M: 1 C: 7
88%
M: 0 C: 1
100%
caseAGreaterNumericBinaryExp(AGreaterNumericBinaryExp, Context)
M: 18 C: 39
68%
M: 3 C: 5
63%
M: 3 C: 2
40%
M: 1 C: 7
88%
M: 0 C: 1
100%
caseAImpliesBooleanBinaryExp(AImpliesBooleanBinaryExp, Context)
M: 8 C: 31
79%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 3 C: 7
70%
M: 0 C: 1
100%
caseAInSetBinaryExp(AInSetBinaryExp, Context)
M: 6 C: 26
81%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 2 C: 4
67%
M: 0 C: 1
100%
caseALessEqualNumericBinaryExp(ALessEqualNumericBinaryExp, Context)
M: 18 C: 39
68%
M: 3 C: 5
63%
M: 3 C: 2
40%
M: 1 C: 7
88%
M: 0 C: 1
100%
caseALessNumericBinaryExp(ALessNumericBinaryExp, Context)
M: 18 C: 39
68%
M: 3 C: 5
63%
M: 3 C: 2
40%
M: 1 C: 7
88%
M: 0 C: 1
100%
caseAMapUnionBinaryExp(AMapUnionBinaryExp, Context)
M: 24 C: 63
72%
M: 3 C: 3
50%
M: 2 C: 2
50%
M: 3 C: 14
82%
M: 0 C: 1
100%
caseAModNumericBinaryExp(AModNumericBinaryExp, Context)
M: 13 C: 40
75%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 3 C: 5
63%
M: 0 C: 1
100%
caseANotEqualBinaryExp(ANotEqualBinaryExp, Context)
M: 0 C: 28
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
caseANotInSetBinaryExp(ANotInSetBinaryExp, Context)
M: 6 C: 30
83%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 2 C: 4
67%
M: 0 C: 1
100%
caseAOrBooleanBinaryExp(AOrBooleanBinaryExp, Context)
M: 8 C: 43
84%
M: 2 C: 6
75%
M: 2 C: 3
60%
M: 3 C: 11
79%
M: 0 C: 1
100%
caseAPlusNumericBinaryExp(APlusNumericBinaryExp, Context)
M: 5 C: 54
92%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 1 C: 12
92%
M: 0 C: 1
100%
caseAPlusPlusBinaryExp(APlusPlusBinaryExp, Context)
M: 19 C: 108
85%
M: 1 C: 9
90%
M: 1 C: 5
83%
M: 2 C: 20
91%
M: 0 C: 1
100%
caseAProperSubsetBinaryExp(AProperSubsetBinaryExp, Context)
M: 7 C: 36
84%
M: 2 C: 2
50%
M: 2 C: 1
33%
M: 2 C: 5
71%
M: 0 C: 1
100%
caseARangeResByBinaryExp(ARangeResByBinaryExp, Context)
M: 6 C: 58
91%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 2 C: 12
86%
M: 0 C: 1
100%
caseARangeResToBinaryExp(ARangeResToBinaryExp, Context)
M: 6 C: 58
91%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 2 C: 12
86%
M: 0 C: 1
100%
caseARemNumericBinaryExp(ARemNumericBinaryExp, Context)
M: 13 C: 38
75%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 3 C: 5
63%
M: 0 C: 1
100%
caseASeqConcatBinaryExp(ASeqConcatBinaryExp, Context)
M: 6 C: 38
86%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 2 C: 7
78%
M: 0 C: 1
100%
caseASetDifferenceBinaryExp(ASetDifferenceBinaryExp, Context)
M: 6 C: 49
89%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 2 C: 9
82%
M: 0 C: 1
100%
caseASetIntersectBinaryExp(ASetIntersectBinaryExp, Context)
M: 6 C: 34
85%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 2 C: 5
71%
M: 0 C: 1
100%
caseASetUnionBinaryExp(ASetUnionBinaryExp, Context)
M: 6 C: 34
85%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 2 C: 5
71%
M: 0 C: 1
100%
caseAStarStarBinaryExp(AStarStarBinaryExp, Context)
M: 45 C: 106
70%
M: 5 C: 11
69%
M: 4 C: 5
56%
M: 5 C: 22
81%
M: 0 C: 1
100%
caseASubsetBinaryExp(ASubsetBinaryExp, Context)
M: 6 C: 28
82%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 2 C: 4
67%
M: 0 C: 1
100%
caseASubtractNumericBinaryExp(ASubtractNumericBinaryExp, Context)
M: 6 C: 53
90%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 2 C: 11
85%
M: 0 C: 1
100%
caseATimesNumericBinaryExp(ATimesNumericBinaryExp, Context)
M: 6 C: 53
90%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 2 C: 11
85%
M: 0 C: 1
100%
div(double, double)
M: 0 C: 22
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
multiplyExact(long, long, Context)
M: 8 C: 4
33%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 2 C: 1
33%
M: 0 C: 1
100%
subtractExact(long, long, Context)
M: 8 C: 4
33%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 2 C: 1
33%
M: 0 C: 1
100%

Coverage

1: package org.overture.interpreter.eval;
2:
3: import org.overture.ast.analysis.AnalysisException;
4: import org.overture.ast.expressions.AAndBooleanBinaryExp;
5: import org.overture.ast.expressions.ACompBinaryExp;
6: import org.overture.ast.expressions.ADivNumericBinaryExp;
7: import org.overture.ast.expressions.ADivideNumericBinaryExp;
8: import org.overture.ast.expressions.ADomainResByBinaryExp;
9: import org.overture.ast.expressions.ADomainResToBinaryExp;
10: import org.overture.ast.expressions.AEqualsBinaryExp;
11: import org.overture.ast.expressions.AEquivalentBooleanBinaryExp;
12: import org.overture.ast.expressions.AGreaterEqualNumericBinaryExp;
13: import org.overture.ast.expressions.AGreaterNumericBinaryExp;
14: import org.overture.ast.expressions.AImpliesBooleanBinaryExp;
15: import org.overture.ast.expressions.AInSetBinaryExp;
16: import org.overture.ast.expressions.ALessEqualNumericBinaryExp;
17: import org.overture.ast.expressions.ALessNumericBinaryExp;
18: import org.overture.ast.expressions.AMapUnionBinaryExp;
19: import org.overture.ast.expressions.AModNumericBinaryExp;
20: import org.overture.ast.expressions.ANotEqualBinaryExp;
21: import org.overture.ast.expressions.ANotInSetBinaryExp;
22: import org.overture.ast.expressions.AOrBooleanBinaryExp;
23: import org.overture.ast.expressions.APlusNumericBinaryExp;
24: import org.overture.ast.expressions.APlusPlusBinaryExp;
25: import org.overture.ast.expressions.AProperSubsetBinaryExp;
26: import org.overture.ast.expressions.ARangeResByBinaryExp;
27: import org.overture.ast.expressions.ARangeResToBinaryExp;
28: import org.overture.ast.expressions.ARemNumericBinaryExp;
29: import org.overture.ast.expressions.ASeqConcatBinaryExp;
30: import org.overture.ast.expressions.ASetDifferenceBinaryExp;
31: import org.overture.ast.expressions.ASetIntersectBinaryExp;
32: import org.overture.ast.expressions.ASetUnionBinaryExp;
33: import org.overture.ast.expressions.AStarStarBinaryExp;
34: import org.overture.ast.expressions.ASubsetBinaryExp;
35: import org.overture.ast.expressions.ASubtractNumericBinaryExp;
36: import org.overture.ast.expressions.ATimesNumericBinaryExp;
37: import org.overture.interpreter.runtime.Context;
38: import org.overture.interpreter.runtime.ValueException;
39: import org.overture.interpreter.runtime.VdmRuntime;
40: import org.overture.interpreter.runtime.VdmRuntimeError;
41: import org.overture.interpreter.values.BooleanValue;
42: import org.overture.interpreter.values.CompFunctionValue;
43: import org.overture.interpreter.values.FunctionValue;
44: import org.overture.interpreter.values.IterFunctionValue;
45: import org.overture.interpreter.values.MapValue;
46: import org.overture.interpreter.values.NumericValue;
47: import org.overture.interpreter.values.SeqValue;
48: import org.overture.interpreter.values.SetValue;
49: import org.overture.interpreter.values.UndefinedValue;
50: import org.overture.interpreter.values.Value;
51: import org.overture.interpreter.values.ValueList;
52: import org.overture.interpreter.values.ValueMap;
53: import org.overture.interpreter.values.ValueSet;
54:
55: public class BinaryExpressionEvaluator extends UnaryExpressionEvaluator
56: {
57:
58:         /*
59:          * Boolean
60:          */
61:
62:         @Override
63:         public Value caseAAndBooleanBinaryExp(AAndBooleanBinaryExp node,
64:                         Context ctxt) throws AnalysisException
65:         {
66:                 // breakpoint.check(location, ctxt);
67:                 node.getLocation().hit(); // Mark as covered
68:
69:                 try
70:                 {
71:                         Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
72:
73:•                        if (lv.isUndefined())
74:                         {
75:                                 return lv;
76:                         }
77:
78:                         boolean lb = lv.boolValue(ctxt);
79:
80:•                        if (!lb)
81:                         {
82:                                 return lv; // Stop after LHS
83:                         }
84:
85:                         Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
86:                         boolean rb = rv.boolValue(ctxt);
87:
88:•                        if (lb && rb)
89:                         {
90:                                 return rv;
91:                         }
92:
93:                         return new BooleanValue(false);
94:                 } catch (ValueException e)
95:                 {
96:                         return VdmRuntimeError.abort(node.getLocation(), e);
97:                 }
98:         }
99:
100:         @Override
101:         public Value caseAEquivalentBooleanBinaryExp(
102:                         AEquivalentBooleanBinaryExp node, Context ctxt)
103:                         throws AnalysisException
104:         {
105:                 // breakpoint.check(location, ctxt);
106:                 node.getLocation().hit(); // Mark as covered
107:
108:                 try
109:                 {
110:                         Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
111:                         Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
112:
113:•                        if (lv.isUndefined() || rv.isUndefined())
114:                         {
115:                                 return new UndefinedValue();
116:                         }
117:
118:•                        return new BooleanValue(lv.boolValue(ctxt) == rv.boolValue(ctxt));
119:                 } catch (ValueException e)
120:                 {
121:                         return VdmRuntimeError.abort(node.getLocation(), e);
122:                 }
123:         }
124:
125:         @Override
126:         public Value caseAImpliesBooleanBinaryExp(AImpliesBooleanBinaryExp node,
127:                         Context ctxt) throws AnalysisException
128:         {
129:                 // breakpoint.check(location, ctxt);
130:                 node.getLocation().hit(); // Mark as covered
131:
132:                 try
133:                 {
134:                         Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
135:
136:•                        if (lv.isUndefined())
137:                         {
138:                                 return lv;
139:                         }
140:
141:                         boolean lb = lv.boolValue(ctxt);
142:
143:•                        if (lb)
144:                         {
145:                                 return node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
146:                         }
147:
148:                         return new BooleanValue(true);
149:                 } catch (ValueException e)
150:                 {
151:                         return VdmRuntimeError.abort(node.getLocation(), e);
152:                 }
153:         }
154:
155:         @Override
156:         public Value caseAOrBooleanBinaryExp(AOrBooleanBinaryExp node, Context ctxt)
157:                         throws AnalysisException
158:         {
159:                 // breakpoint.check(location, ctxt);
160:                 node.getLocation().hit(); // Mark as covered
161:
162:                 try
163:                 {
164:                         Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
165:
166:•                        if (lv.isUndefined())
167:                         {
168:                                 return lv;
169:                         } else
170:                         {
171:                                 boolean lb = lv.boolValue(ctxt);
172:
173:•                                if (lb)
174:                                 {
175:                                         return lv; // Stop after LHS
176:                                 }
177:
178:                                 Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
179:                                 boolean rb = rv.boolValue(ctxt);
180:
181:•                                if (lb || rb)
182:                                 {
183:                                         return new BooleanValue(true);
184:                                 } else
185:                                 {
186:                                         return rv;
187:                                 }
188:                         }
189:                 } catch (ValueException e)
190:                 {
191:                         return VdmRuntimeError.abort(node.getLocation(), e);
192:                 }
193:         }
194:
195:         /*
196:          * end boolean
197:          */
198:
199:         @Override
200:         public Value caseACompBinaryExp(ACompBinaryExp node, Context ctxt)
201:                         throws AnalysisException
202:         {
203:                 // breakpoint.check(location, ctxt);
204:                 node.getLocation().hit(); // Mark as covered
205:
206:                 Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).deref();
207:                 Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).deref();
208:
209:•                if (lv instanceof MapValue)
210:                 {
211:                         ValueMap lm = null;
212:                         ValueMap rm = null;
213:
214:                         try
215:                         {
216:                                 lm = lv.mapValue(ctxt);
217:                                 rm = rv.mapValue(ctxt);
218:                         } catch (ValueException e)
219:                         {
220:                                 return VdmRuntimeError.abort(node.getLocation(), e);
221:                         }
222:
223:                         ValueMap result = new ValueMap();
224:
225:•                        for (Value v : rm.keySet())
226:                         {
227:                                 Value rng = lm.get(rm.get(v));
228:
229:•                                if (rng == null)
230:                                 {
231:                                         VdmRuntimeError.abort(node.getLocation(), 4162, "The RHS range is not a subset of the LHS domain", ctxt);
232:                                 }
233:
234:                                 Value old = result.put(v, rng);
235:
236:•                                if (old != null && !old.equals(rng))
237:                                 {
238:                                         VdmRuntimeError.abort(node.getLocation(), 4005, "Duplicate map keys have different values", ctxt);
239:                                 }
240:                         }
241:
242:                         return new MapValue(result);
243:                 }
244:
245:                 try
246:                 {
247:                         FunctionValue f1 = lv.functionValue(ctxt);
248:                         FunctionValue f2 = rv.functionValue(ctxt);
249:
250:                         return new CompFunctionValue(f1, f2);
251:                 } catch (ValueException e)
252:                 {
253:                         return VdmRuntimeError.abort(node.getLocation(), e);
254:                 }
255:         }
256:
257:         @Override
258:         public Value caseADomainResByBinaryExp(ADomainResByBinaryExp node,
259:                         Context ctxt) throws AnalysisException
260:         {
261:                 // breakpoint.check(location, ctxt);
262:                 node.getLocation().hit(); // Mark as covered
263:
264:                 try
265:                 {
266:                         ValueSet set = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt);
267:                         ValueMap map = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).mapValue(ctxt);
268:                         ValueMap modified = new ValueMap(map);
269:
270:•                        for (Value k : map.keySet())
271:                         {
272:•                                if (set.contains(k))
273:                                 {
274:                                         modified.remove(k);
275:                                 }
276:                         }
277:
278:                         return new MapValue(modified);
279:                 } catch (ValueException e)
280:                 {
281:                         return VdmRuntimeError.abort(node.getLocation(), e);
282:                 }
283:         }
284:
285:         @Override
286:         public Value caseADomainResToBinaryExp(ADomainResToBinaryExp node,
287:                         Context ctxt) throws AnalysisException
288:         {
289:                 // breakpoint.check(location, ctxt);
290:                 node.getLocation().hit(); // Mark as covered
291:
292:                 try
293:                 {
294:                         ValueSet set = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt);
295:                         ValueMap map = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).mapValue(ctxt);
296:                         ValueMap modified = new ValueMap(map);
297:
298:•                        for (Value k : map.keySet())
299:                         {
300:•                                if (!set.contains(k))
301:                                 {
302:                                         modified.remove(k);
303:                                 }
304:                         }
305:
306:                         return new MapValue(modified);
307:                 } catch (ValueException e)
308:                 {
309:                         return VdmRuntimeError.abort(node.getLocation(), e);
310:                 }
311:         }
312:
313:         @Override
314:         public Value caseAEqualsBinaryExp(AEqualsBinaryExp node, Context ctxt)
315:                         throws AnalysisException
316:         {
317:                 // breakpoint.check(location, ctxt);
318:                 node.getLocation().hit(); // Mark as covered
319:
320:                 Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
321:
322:•                if (lv.isUndefined())
323:                 {
324:                         return lv;
325:                 }
326:
327:                 Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
328:
329:•                if (rv.isUndefined())
330:                 {
331:                         return rv;
332:                 }
333:
334:                 return new BooleanValue(lv.equals(rv));
335:         }
336:
337:         @Override
338:         public Value caseAInSetBinaryExp(AInSetBinaryExp node, Context ctxt)
339:                         throws AnalysisException
340:         {
341:                 // breakpoint.check(location, ctxt);
342:                 node.getLocation().hit(); // Mark as covered
343:
344:                 Value elem = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
345:                 Value set = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
346:
347:                 try
348:                 {
349:                         return new BooleanValue(set.setValue(ctxt).contains(elem));
350:                 } catch (ValueException e)
351:                 {
352:                         return VdmRuntimeError.abort(node.getLocation(), e);
353:                 }
354:         }
355:
356:         @Override
357:         public Value caseAMapUnionBinaryExp(AMapUnionBinaryExp node, Context ctxt)
358:                         throws AnalysisException
359:         {
360:                 // breakpoint.check(location, ctxt);
361:                 node.getLocation().hit(); // Mark as covered
362:
363:                 ValueMap lm = null;
364:                 ValueMap rm = null;
365:
366:                 try
367:                 {
368:                         lm = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).mapValue(ctxt);
369:                         rm = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).mapValue(ctxt);
370:                 } catch (ValueException e)
371:                 {
372:                         return VdmRuntimeError.abort(node.getLocation(), e);
373:                 }
374:
375:                 ValueMap result = new ValueMap();
376:                 result.putAll(lm);
377:
378:•                for (Value k : rm.keySet())
379:                 {
380:                         Value rng = rm.get(k);
381:                         Value old = result.put(k, rng);
382:
383:•                        if (old != null && !old.equals(rng))
384:                         {
385:                                 VdmRuntimeError.abort(node.getLocation(), 4021, "Duplicate map keys have different values: "
386:                                                 + k, ctxt);
387:                         }
388:                 }
389:
390:                 return new MapValue(result);
391:         }
392:
393:         @Override
394:         public Value caseANotEqualBinaryExp(ANotEqualBinaryExp node, Context ctxt)
395:                         throws AnalysisException
396:         {
397:                 // breakpoint.check(location, ctxt);
398:                 node.getLocation().hit(); // Mark as covered
399:
400:                 Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
401:                 Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
402:
403:•                return new BooleanValue(!lv.equals(rv));
404:         }
405:
406:         @Override
407:         public Value caseANotInSetBinaryExp(ANotInSetBinaryExp node, Context ctxt)
408:                         throws AnalysisException
409:         {
410:                 // breakpoint.check(location, ctxt);
411:                 node.getLocation().hit(); // Mark as covered
412:
413:                 Value elem = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
414:                 Value set = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
415:
416:                 try
417:                 {
418:•                        return new BooleanValue(!set.setValue(ctxt).contains(elem));
419:                 } catch (ValueException e)
420:                 {
421:                         return VdmRuntimeError.abort(node.getLocation(), e);
422:                 }
423:         }
424:
425:         /*
426:          * Numeric
427:          */
428:
429:         @Override
430:         public Value caseADivNumericBinaryExp(ADivNumericBinaryExp node,
431:                         Context ctxt) throws AnalysisException
432:         {
433:                 // breakpoint.check(location, ctxt);
434:                 node.getLocation().hit(); // Mark as covered
435:
436:                 try
437:                 {
438:                         double lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).intValue(ctxt);
439:                         double rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).intValue(ctxt);
440:
441:•                        if (rv == 0)
442:                         {
443:                                 throw new ValueException(4134, "Infinite or NaN trouble", ctxt);
444:                         }
445:
446:                         return NumericValue.valueOf(div(lv, rv), ctxt);
447:                 } catch (ValueException e)
448:                 {
449:                         return VdmRuntimeError.abort(node.getLocation(), e);
450:                 }
451:         }
452:
453:         @Override
454:         public Value caseADivideNumericBinaryExp(ADivideNumericBinaryExp node,
455:                         Context ctxt) throws AnalysisException
456:         {
457:                 // breakpoint.check(location, ctxt);
458:                 node.getLocation().hit(); // Mark as covered
459:
460:                 try
461:                 {
462:                         double lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).realValue(ctxt);
463:                         double rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).realValue(ctxt);
464:
465:                         return NumericValue.valueOf(lv / rv, ctxt);
466:                 } catch (ValueException e)
467:                 {
468:                         return VdmRuntimeError.abort(node.getLocation(), e);
469:                 }
470:         }
471:
472:         @Override
473:         public Value caseAGreaterEqualNumericBinaryExp(
474:                         AGreaterEqualNumericBinaryExp node, Context ctxt)
475:                         throws AnalysisException
476:         {
477:                 // breakpoint.check(location, ctxt);
478:                 node.getLocation().hit(); // Mark as covered
479:
480:                 Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
481:                 Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
482:
483:•                if (lv.isOrdered() && rv.isOrdered())
484:                 {
485:                         int cmp = lv.compareTo(rv);
486:
487:•                        if (cmp != Integer.MIN_VALUE)        // Indicates comparable
488:                         {
489:•                                return new BooleanValue(cmp >= 0);
490:                         }
491:                 }
492:
493:                 return VdmRuntimeError.abort(node.getLocation(), 4171, "Values cannot be compared: " + lv + ", " + rv, ctxt);
494:         }
495:
496:         @Override
497:         public Value caseAGreaterNumericBinaryExp(AGreaterNumericBinaryExp node,
498:                                                                                          Context ctxt) throws AnalysisException
499:         {
500:                 // breakpoint.check(location, ctxt);
501:                 node.getLocation().hit(); // Mark as covered
502:
503:                 Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
504:                 Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
505:
506:•                if (lv.isOrdered() && rv.isOrdered())
507:                 {
508:                         int cmp = lv.compareTo(rv);
509:
510:•                        if (cmp != Integer.MIN_VALUE)        // Indicates comparable
511:                         {
512:•                                return new BooleanValue(cmp > 0);
513:                         }
514:                 }
515:
516:                 return VdmRuntimeError.abort(node.getLocation(), 4171, "Values cannot be compared: " + lv + ", " + rv, ctxt);
517:         }
518:
519:         @Override
520:         public Value caseALessEqualNumericBinaryExp(
521:                         ALessEqualNumericBinaryExp node, Context ctxt)
522:                         throws AnalysisException
523:         {
524:                 // breakpoint.check(location, ctxt);
525:                 node.getLocation().hit(); // Mark as covered
526:
527:                 Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
528:                 Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
529:
530:•                if (lv.isOrdered() && rv.isOrdered())
531:                 {
532:                         int cmp = lv.compareTo(rv);
533:
534:•                        if (cmp != Integer.MIN_VALUE)        // Indicates comparable
535:                         {
536:•                                return new BooleanValue(cmp <= 0);
537:                         }
538:                 }
539:
540:                 return VdmRuntimeError.abort(node.getLocation(), 4171, "Values cannot be compared: " + lv + ", " + rv, ctxt);
541:         }
542:
543:         @Override
544:         public Value caseALessNumericBinaryExp(ALessNumericBinaryExp node,
545:                                                                                  Context ctxt) throws AnalysisException
546:         {
547:                 // breakpoint.check(location, ctxt);
548:                 node.getLocation().hit(); // Mark as covered
549:
550:                 Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
551:                 Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
552:
553:•                if (lv.isOrdered() && rv.isOrdered())
554:                 {
555:                         int cmp = lv.compareTo(rv);
556:
557:•                        if (cmp != Integer.MIN_VALUE)        // Indicates comparable
558:                         {
559:•                                return new BooleanValue(cmp < 0);
560:                         }
561:                 }
562:
563:                 return VdmRuntimeError.abort(node.getLocation(), 4171, "Values cannot be compared: " + lv + ", " + rv, ctxt);
564:         }
565:         @Override
566:         public Value caseAModNumericBinaryExp(AModNumericBinaryExp node,
567:                         Context ctxt) throws AnalysisException
568:         {
569:                 // breakpoint.check(location, ctxt);
570:                 node.getLocation().hit(); // Mark as covered
571:
572:                 try
573:                 {
574:                         /*
575:                          * Remainder x rem y and modulus x mod y are the same if the signs of x and y are the same, otherwise they
576:                          * differ and rem takes the sign of x and mod takes the sign of y. The formulas for remainder and modulus
577:                          * are: x rem y = x - y * (x div y) x mod y = x - y * floor(x/y) Hence, -14 rem 3 equals -2 and -14 mod 3
578:                          * equals 1. One can view these results by walking the real axis, starting at -14 and making jumps of 3. The
579:                          * remainder will be the last negative number one visits, because the first argument corresponding to x is
580:                          * negative, while the modulus will be the first positive number one visit, because the second argument
581:                          * corresponding to y is positive.
582:                          */
583:
584:                         double lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).intValue(ctxt);
585:                         double rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).intValue(ctxt);
586:
587:•                        if (rv == 0)
588:                         {
589:                                 throw new ValueException(4134, "Infinite or NaN trouble", ctxt);
590:                         }
591:
592:                         return NumericValue.valueOf(lv - rv * (long) Math.floor(lv / rv), ctxt);
593:                 } catch (ValueException e)
594:                 {
595:                         return VdmRuntimeError.abort(node.getLocation(), e);
596:                 }
597:         }
598:
599:         @Override
600:         public Value caseAPlusNumericBinaryExp(APlusNumericBinaryExp node,
601:                         Context ctxt) throws AnalysisException
602:         {
603:                 // breakpoint.check(location, ctxt);
604:                 node.getLocation().hit(); // Mark as covered
605:
606:                 try
607:                 {
608:                 Value l = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
609:                 Value r = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
610:
611:•                        if (NumericValue.areIntegers(l, r))
612:                         {
613:                                 long lv = l.intValue(ctxt);
614:                                 long rv = r.intValue(ctxt);
615:                                 long sum = addExact(lv, rv, ctxt);
616:                                 return NumericValue.valueOf(sum, ctxt);
617:                         }
618:                         else
619:                         {
620:                                 double lv = l.realValue(ctxt);
621:                                 double rv = r.realValue(ctxt);
622:                          return NumericValue.valueOf(lv + rv, ctxt);
623:                         }
624:
625:                 } catch (ValueException e)
626:                 {
627:                         return VdmRuntimeError.abort(node.getLocation(), e);
628:                 }
629:         }
630:
631:         @Override
632:         public Value caseARemNumericBinaryExp(ARemNumericBinaryExp node,
633:                         Context ctxt) throws AnalysisException
634:         {
635:                 // breakpoint.check(location, ctxt);
636:                 node.getLocation().hit(); // Mark as covered
637:
638:                 try
639:                 {
640:                         /*
641:                          * Remainder x rem y and modulus x mod y are the same if the signs of x and y are the same, otherwise they
642:                          * differ and rem takes the sign of x and mod takes the sign of y. The formulas for remainder and modulus
643:                          * are: x rem y = x - y * (x div y) x mod y = x - y * floor(x/y) Hence, -14 rem 3 equals -2 and -14 mod 3
644:                          * equals 1. One can view these results by walking the real axis, starting at -14 and making jumps of 3. The
645:                          * remainder will be the last negative number one visits, because the first argument corresponding to x is
646:                          * negative, while the modulus will be the first positive number one visit, because the second argument
647:                          * corresponding to y is positive.
648:                          */
649:
650:                         double lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).intValue(ctxt);
651:                         double rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).intValue(ctxt);
652:
653:•                        if (rv == 0)
654:                         {
655:                                 throw new ValueException(4134, "Infinite or NaN trouble", ctxt);
656:                         }
657:
658:                         return NumericValue.valueOf(lv - rv * div(lv, rv), ctxt);
659:                 } catch (ValueException e)
660:                 {
661:                         return VdmRuntimeError.abort(node.getLocation(), e);
662:                 }
663:         }
664:
665:         @Override
666:         public Value caseASubtractNumericBinaryExp(ASubtractNumericBinaryExp node,
667:                         Context ctxt) throws AnalysisException
668:         {
669:                 // breakpoint.check(location, ctxt);
670:                 node.getLocation().hit(); // Mark as covered
671:
672:                 try
673:                 {
674:                 Value l = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
675:                 Value r = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
676:
677:•                        if (NumericValue.areIntegers(l, r))
678:                         {
679:                                 long lv = l.intValue(ctxt);
680:                                 long rv = r.intValue(ctxt);
681:                                 long diff = subtractExact(lv, rv, ctxt);
682:                                 return NumericValue.valueOf(diff, ctxt);
683:                         }
684:                         else
685:                         {
686:                                 double lv = l.realValue(ctxt);
687:                                 double rv = r.realValue(ctxt);
688:                          return NumericValue.valueOf(lv - rv, ctxt);
689:                         }
690:                 } catch (ValueException e)
691:                 {
692:                         return VdmRuntimeError.abort(node.getLocation(), e);
693:                 }
694:         }
695:
696:         @Override
697:         public Value caseATimesNumericBinaryExp(ATimesNumericBinaryExp node,
698:                         Context ctxt) throws AnalysisException
699:         {
700:                 // breakpoint.check(location, ctxt);
701:                 node.getLocation().hit(); // Mark as covered
702:
703:                 try
704:                 {
705:                 Value l = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
706:                 Value r = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
707:
708:•                        if (NumericValue.areIntegers(l, r))
709:                         {
710:                                 long lv = l.intValue(ctxt);
711:                                 long rv = r.intValue(ctxt);
712:                                 long mult = multiplyExact(lv, rv, ctxt);
713:                                 return NumericValue.valueOf(mult, ctxt);
714:                         }
715:                         else
716:                         {
717:                                 double lv = l.realValue(ctxt);
718:                                 double rv = r.realValue(ctxt);
719:                          return NumericValue.valueOf(lv * rv, ctxt);
720:                         }
721:                 } catch (ValueException e)
722:                 {
723:                         return VdmRuntimeError.abort(node.getLocation(), e);
724:                 }
725:         }
726:
727:         /*
728:          * end numeric
729:          */
730:
731:         @Override
732:         public Value caseAPlusPlusBinaryExp(APlusPlusBinaryExp node, Context ctxt)
733:                         throws AnalysisException
734:         {
735:                 // breakpoint.check(location, ctxt);
736:                 node.getLocation().hit(); // Mark as covered
737:
738:                 try
739:                 {
740:                         Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).deref();
741:                         Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
742:
743:•                        if (lv instanceof MapValue)
744:                         {
745:                                 ValueMap lm = new ValueMap(lv.mapValue(ctxt));
746:                                 ValueMap rm = rv.mapValue(ctxt);
747:
748:•                                for (Value k : rm.keySet())
749:                                 {
750:                                         lm.put(k, rm.get(k));
751:                                 }
752:
753:                                 return new MapValue(lm);
754:                         } else
755:                         {
756:                                 ValueList seq = lv.seqValue(ctxt);
757:                                 ValueMap map = rv.mapValue(ctxt);
758:                                 ValueList result = new ValueList(seq);
759:
760:•                                for (Value k : map.keySet())
761:                                 {
762:                                         int iv = (int) k.intValue(ctxt);
763:
764:•                                        if (iv < 1 || iv > seq.size())
765:                                         {
766:                                                 VdmRuntimeError.abort(node.getLocation(), 4025, "Map key not within sequence index range: "
767:                                                                 + k, ctxt);
768:                                         }
769:
770:                                         result.set(iv - 1, map.get(k));
771:                                 }
772:
773:                                 return new SeqValue(result);
774:                         }
775:                 } catch (ValueException e)
776:                 {
777:                         return VdmRuntimeError.abort(node.getLocation(), e);
778:                 }
779:         }
780:
781:         @Override
782:         public Value caseAProperSubsetBinaryExp(AProperSubsetBinaryExp node,
783:                         Context ctxt) throws AnalysisException
784:         {
785:                 // breakpoint.check(location, ctxt);
786:                 node.getLocation().hit(); // Mark as covered
787:
788:                 try
789:                 {
790:                         ValueSet set1 = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt);
791:                         ValueSet set2 = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt);
792:
793:•                        return new BooleanValue(set1.size() < set2.size()
794:•                                        && set2.containsAll(set1));
795:                 } catch (ValueException e)
796:                 {
797:                         return VdmRuntimeError.abort(node.getLocation(), e);
798:                 }
799:         }
800:
801:         @Override
802:         public Value caseARangeResByBinaryExp(ARangeResByBinaryExp node,
803:                         Context ctxt) throws AnalysisException
804:         {
805:                 // breakpoint.check(location, ctxt);
806:                 node.getLocation().hit(); // Mark as covered
807:
808:                 ValueSet set = null;
809:                 ValueMap map = null;
810:
811:                 try
812:                 {
813:                         set = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt);
814:                         map = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).mapValue(ctxt);
815:                 } catch (ValueException e)
816:                 {
817:                         return VdmRuntimeError.abort(node.getLocation(), e);
818:                 }
819:
820:                 ValueMap modified = new ValueMap(map);
821:
822:•                for (Value k : map.keySet())
823:                 {
824:•                        if (set.contains(map.get(k)))
825:                         {
826:                                 modified.remove(k);
827:                         }
828:                 }
829:
830:                 return new MapValue(modified);
831:         }
832:
833:         @Override
834:         public Value caseARangeResToBinaryExp(ARangeResToBinaryExp node,
835:                         Context ctxt) throws AnalysisException
836:         {
837:                 // breakpoint.check(location, ctxt);
838:                 node.getLocation().hit(); // Mark as covered
839:
840:                 ValueSet set = null;
841:                 ValueMap map = null;
842:
843:                 try
844:                 {
845:                         set = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt);
846:                         map = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).mapValue(ctxt);
847:                 } catch (ValueException e)
848:                 {
849:                         return VdmRuntimeError.abort(node.getLocation(), e);
850:                 }
851:
852:                 ValueMap modified = new ValueMap(map);
853:
854:•                for (Value k : map.keySet())
855:                 {
856:•                        if (!set.contains(map.get(k)))
857:                         {
858:                                 modified.remove(k);
859:                         }
860:                 }
861:
862:                 return new MapValue(modified);
863:         }
864:
865:         @Override
866:         public Value caseASeqConcatBinaryExp(ASeqConcatBinaryExp node, Context ctxt)
867:                         throws AnalysisException
868:         {
869:                 // breakpoint.check(location, ctxt);
870:                 node.getLocation().hit(); // Mark as covered
871:
872:                 try
873:                 {
874:                         Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
875:                         Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
876:
877:                         ValueList result = new ValueList();
878:                         result.addAll(lv.seqValue(ctxt));
879:                         result.addAll(rv.seqValue(ctxt));
880:
881:                         return new SeqValue(result);
882:                 } catch (ValueException e)
883:                 {
884:                         return VdmRuntimeError.abort(node.getLocation(), e);
885:                 }
886:         }
887:
888:         @Override
889:         public Value caseASetDifferenceBinaryExp(ASetDifferenceBinaryExp node,
890:                         Context ctxt) throws AnalysisException
891:         {
892:                 // breakpoint.check(location, ctxt);
893:                 node.getLocation().hit(); // Mark as covered
894:
895:                 ValueSet result = new ValueSet();
896:                 ValueSet togo = null;
897:
898:                 try
899:                 {
900:                         togo = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt);
901:                         result.addAll(node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt));
902:
903:•                        for (Value r : togo)
904:                         {
905:                                 result.remove(r);
906:                         }
907:
908:                         return new SetValue(result);
909:                 }
910:                 catch (ValueException e)
911:                 {
912:                         return VdmRuntimeError.abort(node.getLocation(), e);
913:                 }
914:         }
915:
916:         @Override
917:         public Value caseASetIntersectBinaryExp(ASetIntersectBinaryExp node,
918:                         Context ctxt) throws AnalysisException
919:         {
920:                 // breakpoint.check(location, ctxt);
921:                 node.getLocation().hit(); // Mark as covered
922:
923:                 try
924:                 {
925:                         ValueSet result = new ValueSet();
926:                         result.addAll(node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt));
927:                         result.retainAll(node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt));
928:                         return new SetValue(result);
929:                 } catch (ValueException e)
930:                 {
931:                         return VdmRuntimeError.abort(node.getLocation(), e);
932:                 }
933:         }
934:
935:         @Override
936:         public Value caseASetUnionBinaryExp(ASetUnionBinaryExp node, Context ctxt)
937:                         throws AnalysisException
938:         {
939:                 // breakpoint.check(location, ctxt);
940:                 node.getLocation().hit(); // Mark as covered
941:
942:                 try
943:                 {
944:                         ValueSet result = new ValueSet();
945:                         result.addAll(node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt));
946:                         result.addAll(node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt));
947:                         return new SetValue(result);
948:                 } catch (ValueException e)
949:                 {
950:                         return VdmRuntimeError.abort(node.getLocation(), e);
951:                 }
952:         }
953:
954:         @Override
955:         public Value caseAStarStarBinaryExp(AStarStarBinaryExp node, Context ctxt)
956:                         throws AnalysisException
957:         {
958:                 // breakpoint.check(location, ctxt);
959:                 node.getLocation().hit(); // Mark as covered
960:
961:                 try
962:                 {
963:                         Value lv = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).deref();
964:                         Value rv = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt);
965:
966:•                        if (lv instanceof MapValue)
967:                         {
968:                                 ValueMap map = lv.mapValue(ctxt);
969:                                 long n = rv.intValue(ctxt);
970:                                 ValueMap result = new ValueMap();
971:
972:•                                for (Value k : map.keySet())
973:                                 {
974:                                         Value r = k;
975:
976:•                                        for (int i = 0; i < n; i++)
977:                                         {
978:                                                 r = map.get(r);
979:                                         }
980:
981:•                                        if (r == null)
982:                                         {
983:                                                 VdmRuntimeError.abort(node.getLocation(), 4133, "Map range is not a subset of its domain: "
984:                                                                 + k, ctxt);
985:                                         }
986:
987:                                         Value old = result.put(k, r);
988:
989:•                                        if (old != null && !old.equals(r))
990:                                         {
991:                                                 VdmRuntimeError.abort(node.getLocation(), 4030, "Duplicate map keys have different values: "
992:                                                                 + k, ctxt);
993:                                         }
994:                                 }
995:
996:                                 return new MapValue(result);
997:•                        } else if (lv instanceof FunctionValue)
998:                         {
999:                                 return new IterFunctionValue(lv.functionValue(ctxt), rv.intValue(ctxt));
1000:•                        } else if (lv instanceof NumericValue)
1001:                         {
1002:                                 double ld = lv.realValue(ctxt);
1003:                                 double rd = rv.realValue(ctxt);
1004:
1005:                                 return NumericValue.valueOf(Math.pow(ld, rd), ctxt);
1006:                         }
1007:
1008:                         return VdmRuntimeError.abort(node.getLocation(), 4031, "First arg of '**' must be a map, function or number", ctxt);
1009:                 } catch (ValueException e)
1010:                 {
1011:                         return VdmRuntimeError.abort(node.getLocation(), e);
1012:                 }
1013:         }
1014:
1015:         @Override
1016:         public Value caseASubsetBinaryExp(ASubsetBinaryExp node, Context ctxt)
1017:                         throws AnalysisException
1018:         {
1019:                 // breakpoint.check(location, ctxt);
1020:                 node.getLocation().hit(); // Mark as covered
1021:
1022:                 try
1023:                 {
1024:                         ValueSet set1 = node.getLeft().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt);
1025:                         ValueSet set2 = node.getRight().apply(VdmRuntime.getExpressionEvaluator(), ctxt).setValue(ctxt);
1026:
1027:                         return new BooleanValue(set2.containsAll(set1));
1028:                 } catch (ValueException e)
1029:                 {
1030:                         return VdmRuntimeError.abort(node.getLocation(), e);
1031:                 }
1032:         }
1033:
1034:         /*
1035:          * Utility methods
1036:          */
1037:
1038:         static public long div(double lv, double rv)
1039:         {
1040:                 /*
1041:                  * There is often confusion on how integer division, remainder and modulus work on negative numbers. In fact,
1042:                  * there are two valid answers to -14 div 3: either (the intuitive) -4 as in the Toolbox, or -5 as in e.g.
1043:                  * Standard ML [Paulson91]. It is therefore appropriate to explain these operations in some detail. Integer
1044:                  * division is defined using floor and real number division: x/y < 0: x div y = -floor(abs(-x/y)) x/y >= 0: x
1045:                  * div y = floor(abs(x/y)) Note that the order of floor and abs on the right-hand side makes a difference, the
1046:                  * above example would yield -5 if we changed the order. This is because floor always yields a smaller (or
1047:                  * equal) integer, e.g. floor (14/3) is 4 while floor (-14/3) is -5.
1048:                  */
1049:
1050:•                if (lv / rv < 0)
1051:                 {
1052:                         return (long) -Math.floor(Math.abs(lv / rv));
1053:                 } else
1054:                 {
1055:                         return (long) Math.floor(Math.abs(-lv / rv));
1056:                 }
1057:         }
1058:         
1059:         private long addExact(long x, long y, Context ctxt) throws ValueException
1060:         {
1061:                 try
1062:                 {
1063:                         return Math.addExact(x, y);
1064:                 }
1065:                 catch (ArithmeticException e)
1066:                 {
1067:                         throw new ValueException(4169, "Arithmetic overflow", ctxt);
1068:                 }
1069:         }
1070:
1071:         private long subtractExact(long x, long y, Context ctxt) throws ValueException
1072:         {
1073:                 try
1074:                 {
1075:                         return Math.subtractExact(x, y);
1076:                 }
1077:                 catch (ArithmeticException e)
1078:                 {
1079:                         throw new ValueException(4169, "Arithmetic overflow", ctxt);
1080:                 }
1081:         }
1082:
1083: private long multiplyExact(long x, long y, Context ctxt) throws ValueException
1084: {
1085:                 try
1086:                 {
1087:                         return Math.multiplyExact(x, y);
1088:                 }
1089:                 catch (ArithmeticException e)
1090:                 {
1091:                         throw new ValueException(4169, "Arithmetic overflow", ctxt);
1092:                 }
1093: }
1094: }