Package: IsaPog

IsaPog

nameinstructionbranchcomplexitylinemethod
IsaPog(List)
M: 0 C: 55
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
getErrorMessage()
M: 36 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 7 C: 0
0%
M: 1 C: 0
0%
getModelThyName()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getModelThyString()
M: 4 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getPosThyName()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getPosThyString()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
hasErrors()
M: 16 C: 0
0%
M: 6 C: 0
0%
M: 4 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
makePoLemma(IProofObligation)
M: 0 C: 72
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 17
100%
M: 0 C: 1
100%
makePosThy(IProofObligationList, String)
M: 0 C: 42
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
makePosThyHeader(String)
M: 0 C: 47
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
writeThyFiles(String)
M: 0 C: 38
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%

Coverage

1: package org.overture.isapog;
2:
3: import java.io.File;
4: import java.io.IOException;
5: import java.util.Iterator;
6: import java.util.List;
7:
8: import org.apache.commons.io.FileUtils;
9: import org.overture.ast.analysis.AnalysisException;
10: import org.overture.ast.node.INode;
11: import org.overture.codegen.utils.GeneratedData;
12: import org.overture.codegen.utils.GeneratedModule;
13: import org.overture.pog.pub.IProofObligation;
14: import org.overture.pog.pub.IProofObligationList;
15: import org.overture.pog.pub.ProofObligationGenerator;
16: import org.overturetool.cgisa.IsaGen;
17:
18: /**
19: * Main class for Isabelle Translation and POG integration. <br>
20: * <br>
21: * Usage: instantiate the class with the module you wish to analyse. THen use {@link #getModelThyString()} and
22: * {@link #getPosThyString()} to obtain the Strings for the model and POs translations respectively. <br>
23: * You can also use {@link #writeThyFiles(String)} to write the theory files directly.
24: *
25: * @author ldc
26: */
27: public class IsaPog
28: {
29:
30:         private static final String POS_THY = "_POs";
31:         private static final String ISA_THEORY = "theory";
32:         private static final String ISA_IMPORTS = "imports";
33:         private static final String SINGLE_SPACE = " ";
34:         private static final String LINEBREAK = "\n";
35:         private static final String ISA_BEGIN = "begin\n";
36:         private static final String ISA_END = "end";
37:         private static final String ISA_LEMMA = "lemma";
38:         private static final String BY_TAC = " by vdm_auto_tac";
39:         private static final String THY_EXT = ".thy";
40:         private static final String ISA_OPEN_COMMENT = "(*";
41:         private static final String ISA_CLOSE_COMMENT = "*)";
42:
43:         private GeneratedModule modelThy;
44:         private String modelThyName;
45:         private String posThy;
46:         private String posThyName;
47:
48:         public IsaPog(List<INode> ast) throws AnalysisException,
49:                         org.overture.codegen.ir.analysis.AnalysisException
50:         {
51:                 IProofObligationList pos = ProofObligationGenerator.generateProofObligations(ast);
52:                 pos.renumber();
53:                 IsaGen ig = new IsaGen();
54:
55:                 modelThy = ig.generate(ast).getClasses().get(0);
56:                 modelThyName = modelThy.getName() + THY_EXT;
57:                 posThy = makePosThy(pos, modelThy.getName());
58:                 posThyName = modelThy.getName() + POS_THY + THY_EXT;
59:         }
60:
61:         public String getModelThyString()
62:         {
63:                 return modelThy.getContent();
64:         }
65:
66:         public String getPosThyString()
67:         {
68:                 return posThy;
69:         }
70:
71:         public String getModelThyName()
72:         {
73:                 return modelThyName;
74:         }
75:
76:         public String getPosThyName()
77:         {
78:                 return posThyName;
79:         }
80:
81:         public boolean hasErrors()
82:         {
83:•                return modelThy.hasMergeErrors() || modelThy.hasUnsupportedIrNodes()
84:•                                || modelThy.hasUnsupportedTargLangNodes();
85:         }
86:
87:         public String getErrorMessage()
88:         {
89:                 StringBuilder sb = new StringBuilder();
90:                 sb.append(modelThy.getMergeErrors().toString());
91:                 sb.append(LINEBREAK);
92:                 sb.append(modelThy.getUnsupportedInIr().toString());
93:                 sb.append(LINEBREAK);
94:                 sb.append(modelThy.getUnsupportedInTargLang().toString());
95:                 return sb.toString();
96:         }
97:
98:         /**
99:          * Write Isabelle theory files to disk for the model and proof obligations
100:          *
101:          * @param path
102:          * Path to the directory to write the files to. Must end with the {@link File#separatorChar}
103:          * @return true if write is successful
104:          * @throws IOException
105:          */
106:         public Boolean writeThyFiles(String path) throws IOException
107:         {
108:                 File modelThyFile = new File(path + modelThyName);
109:                 FileUtils.writeStringToFile(modelThyFile, modelThy.getContent());
110:
111:                 File posThyFile = new File(path + posThyName);
112:                 FileUtils.writeStringToFile(posThyFile, posThy);
113:
114:                 return true;
115:         }
116:
117:         private String makePosThyHeader(String moduleName)
118:         {
119:                 StringBuilder sb = new StringBuilder();
120:                 sb.append(ISA_THEORY);
121:                 sb.append(SINGLE_SPACE);
122:                 sb.append(moduleName);
123:                 sb.append(POS_THY);
124:                 sb.append(LINEBREAK);
125:                 sb.append(ISA_IMPORTS);
126:                 sb.append(SINGLE_SPACE);
127:                 sb.append(moduleName);
128:                 sb.append(LINEBREAK);
129:                 sb.append(ISA_BEGIN);
130:                 return sb.toString();
131:         }
132:
133:         private String makePoLemma(IProofObligation po) throws AnalysisException,
134:                         org.overture.codegen.ir.analysis.AnalysisException
135:         {
136:                 StringBuilder sb = new StringBuilder();
137:                 sb.append(ISA_OPEN_COMMENT);
138:                 sb.append(" ");
139:                 sb.append(po.toString());
140:                 sb.append(" ");
141:                 sb.append(ISA_CLOSE_COMMENT);
142:                 sb.append(LINEBREAK);
143:                 sb.append(ISA_LEMMA);
144:                 sb.append(SINGLE_SPACE);
145:                 sb.append(po.getIsaName());
146:                 sb.append(": ");
147:                 sb.append("\"+|");
148:                 sb.append(IsaGen.vdmExp2IsaString(po.getValueTree().getPredicate()));
149:                 sb.append("|+\"");
150:                 sb.append(BY_TAC);
151:                 sb.append(LINEBREAK);
152:                 return sb.toString();
153:         }
154:
155:         private String makePosThy(IProofObligationList pos, String moduleName)
156:                         throws AnalysisException,
157:                         org.overture.codegen.ir.analysis.AnalysisException
158:         {
159:                 StringBuilder sb = new StringBuilder();
160:                 sb.append(makePosThyHeader(moduleName));
161:                 sb.append(LINEBREAK);
162:                 Iterator<IProofObligation> iter = pos.iterator();
163:                 IProofObligation po;
164:
165:•                while (iter.hasNext())
166:                 {
167:                         po = iter.next();
168:                         sb.append(makePoLemma(po));
169:                         sb.append(LINEBREAK);
170:                 }
171:                 sb.append(ISA_END);
172:                 return sb.toString();
173:         }
174:
175: }