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.overturetool.vdmj.expressions;
25
26 import org.overturetool.vdmj.lex.LexToken;
27 import org.overturetool.vdmj.pog.POContextStack;
28 import org.overturetool.vdmj.pog.POImpliesContext;
29 import org.overturetool.vdmj.pog.ProofObligationList;
30 import org.overturetool.vdmj.pog.SubTypeObligation;
31 import org.overturetool.vdmj.runtime.Context;
32 import org.overturetool.vdmj.runtime.ValueException;
33 import org.overturetool.vdmj.types.BooleanType;
34 import org.overturetool.vdmj.values.BooleanValue;
35 import org.overturetool.vdmj.values.Value;
36
37 public class AndExpression extends BooleanBinaryExpression
38 {
39 private static final long serialVersionUID = 1L;
40
41 public AndExpression(Expression left, LexToken op, Expression right)
42 {
43 super(left, op, right);
44 }
45
46 @Override
47 public Value eval(Context ctxt)
48 {
49 breakpoint.check(location, ctxt);
50
51 try
52 {
53 Value lv = left.eval(ctxt);
54
55 if (lv.isUndefined())
56 {
57 return lv;
58 }
59
60 boolean lb = lv.boolValue(ctxt);
61
62 if (!lb)
63 {
64 return lv;
65 }
66
67 Value rv = right.eval(ctxt);
68
69 if (lb)
70 {
71 return rv;
72 }
73
74 return new BooleanValue(false);
75 }
76 catch (ValueException e)
77 {
78 return abort(e);
79 }
80 }
81
82 @Override
83 public ProofObligationList getProofObligations(POContextStack ctxt)
84 {
85 ProofObligationList obligations = new ProofObligationList();
86
87 if (ltype.isUnion())
88 {
89 obligations.add(
90 new SubTypeObligation(left, new BooleanType(left.location), ltype, ctxt));
91 }
92
93 if (rtype.isUnion())
94 {
95 ctxt.push(new POImpliesContext(left));
96 obligations.add(new SubTypeObligation(
97 right, new BooleanType(right.location), rtype, ctxt));
98 ctxt.pop();
99 }
100
101 obligations.addAll(left.getProofObligations(ctxt));
102
103 ctxt.push(new POImpliesContext(left));
104 obligations.addAll(right.getProofObligations(ctxt));
105 ctxt.pop();
106
107 return obligations;
108 }
109
110 @Override
111 public String kind()
112 {
113 return "and";
114 }
115 }