Menu
▾
▴
[Jcontracts-svn] SF.net SVN: jcontracts: [34] trunk/source/java/net/sf/jcontracts/icontract
|
From: <js...@us...> - 2006-11-27 20:14:52
|
Revision: 34
http://svn.sourceforge.net/jcontracts/?rev=34&view=rev
Author: jstuyts
Date: 2006-11-27 12:14:50 -0800 (Mon, 27 Nov 2006)
Log Message:
-----------
Formatted code.
Modified Paths:
--------------
trunk/source/java/net/sf/jcontracts/icontract/AllFilesUpToDateException.java
trunk/source/java/net/sf/jcontracts/icontract/AllOption.java
trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java
trunk/source/java/net/sf/jcontracts/icontract/AssertionExpression.java
trunk/source/java/net/sf/jcontracts/icontract/Class.java
trunk/source/java/net/sf/jcontracts/icontract/CleanOption.java
trunk/source/java/net/sf/jcontracts/icontract/CompilerOption.java
trunk/source/java/net/sf/jcontracts/icontract/Constants.java
trunk/source/java/net/sf/jcontracts/icontract/Darwin.java
trunk/source/java/net/sf/jcontracts/icontract/DefaultExceptionOption.java
trunk/source/java/net/sf/jcontracts/icontract/FileTarget.java
trunk/source/java/net/sf/jcontracts/icontract/HelpOption.java
trunk/source/java/net/sf/jcontracts/icontract/IContracted.java
trunk/source/java/net/sf/jcontracts/icontract/Interface.java
trunk/source/java/net/sf/jcontracts/icontract/Internal0Option.java
trunk/source/java/net/sf/jcontracts/icontract/InvCheck.java
trunk/source/java/net/sf/jcontracts/icontract/InvCheckCallOption.java
trunk/source/java/net/sf/jcontracts/icontract/MergeOption.java
trunk/source/java/net/sf/jcontracts/icontract/MetaclassFactory.java
trunk/source/java/net/sf/jcontracts/icontract/Method.java
trunk/source/java/net/sf/jcontracts/icontract/NoInitialCompilationOption.java
trunk/source/java/net/sf/jcontracts/icontract/NoRepositoryCompilationOption.java
trunk/source/java/net/sf/jcontracts/icontract/OneOneOption.java
trunk/source/java/net/sf/jcontracts/icontract/Option.java
trunk/source/java/net/sf/jcontracts/icontract/OutputOption.java
trunk/source/java/net/sf/jcontracts/icontract/ParameterOption.java
trunk/source/java/net/sf/jcontracts/icontract/PrePostCheck.java
trunk/source/java/net/sf/jcontracts/icontract/ProcessingOption.java
trunk/source/java/net/sf/jcontracts/icontract/QuietOption.java
trunk/source/java/net/sf/jcontracts/icontract/Repository.java
trunk/source/java/net/sf/jcontracts/icontract/RepositoryOutputOption.java
trunk/source/java/net/sf/jcontracts/icontract/SourceCompilerOption.java
trunk/source/java/net/sf/jcontracts/icontract/SystemInTarget.java
trunk/source/java/net/sf/jcontracts/icontract/Target.java
trunk/source/java/net/sf/jcontracts/icontract/Tool.java
trunk/source/java/net/sf/jcontracts/icontract/UnableToDetermineTypeException.java
trunk/source/java/net/sf/jcontracts/icontract/Variable.java
trunk/source/java/net/sf/jcontracts/icontract/VerboseOption.java
trunk/source/java/net/sf/jcontracts/icontract/WrapExceptionOption.java
trunk/source/java/net/sf/jcontracts/icontract/XOption.java
Modified: trunk/source/java/net/sf/jcontracts/icontract/AllFilesUpToDateException.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/AllFilesUpToDateException.java 2006-11-27 16:56:26 UTC (rev 33)
+++ trunk/source/java/net/sf/jcontracts/icontract/AllFilesUpToDateException.java 2006-11-27 20:14:50 UTC (rev 34)
@@ -1,11 +1,14 @@
package net.sf.jcontracts.icontract;
-
-public class AllFilesUpToDateException extends RuntimeException {
-
- public AllFilesUpToDateException() {
- }
-
- public AllFilesUpToDateException(String s) {
- super(s);
- }
-}
+
+public class AllFilesUpToDateException extends RuntimeException
+{
+
+ public AllFilesUpToDateException()
+ {
+ }
+
+ public AllFilesUpToDateException(String s)
+ {
+ super(s);
+ }
+}
Modified: trunk/source/java/net/sf/jcontracts/icontract/AllOption.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/AllOption.java 2006-11-27 16:56:26 UTC (rev 33)
+++ trunk/source/java/net/sf/jcontracts/icontract/AllOption.java 2006-11-27 20:14:50 UTC (rev 34)
@@ -1,12 +1,14 @@
package net.sf.jcontracts.icontract;
import java.util.Vector;
-
-public class AllOption extends ParameterOption {
-
- public static final String NAME = "a";
-
- public AllOption(String name, Vector arguments) {
- super(name, arguments);
- }
-}
+
+public class AllOption extends ParameterOption
+{
+
+ public static final String NAME = "a";
+
+ public AllOption(String name, Vector arguments)
+ {
+ super(name, arguments);
+ }
+}
Modified: trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java 2006-11-27 16:56:26 UTC (rev 33)
+++ trunk/source/java/net/sf/jcontracts/icontract/ArgMetaclassFactory.java 2006-11-27 20:14:50 UTC (rev 34)
@@ -5,80 +5,107 @@
import net.sf.jcontracts.argparser.OptionMetaclass;
import net.sf.jcontracts.argparser.ParserMetaclassFactory;
import net.sf.jcontracts.argparser.TargetMetaclass;
-
-public class ArgMetaclassFactory
- implements ParserMetaclassFactory {
-
- public OptionMetaclass newOption(String name, Vector parameters) {
- OptionMetaclass o = null;
- try {
- if (name.compareTo("h") == 0) {
- o = new HelpOption(name, parameters);
- } else
- if (name.compareTo("v") == 0) {
- o = new VerboseOption(name, parameters);
- } else
- if (name.compareTo("c") == 0) {
- o = new CompilerOption(name, parameters);
- } else
- if (name.compareTo("b") == 0) {
- o = new SourceCompilerOption(name, parameters);
- } else
- if (name.compareTo("n") == 0) {
- o = new NoRepositoryCompilationOption(name, parameters);
- } else
- if (name.compareTo("o") == 0) {
- o = new OutputOption(name, parameters);
- } else
- if (name.compareTo("y") == 0) {
- o = new OneOneOption(name, parameters);
- } else
- if (name.compareTo("k") == 0) {
- o = new RepositoryOutputOption(name, parameters);
- } else
- if (name.compareTo("d") == 0) {
- o = new DefaultExceptionOption(name, parameters);
- } else
- if (name.compareTo("r") == 0) {
- o = new CleanOption(name, parameters);
- } else
- if (name.compareTo("m") == 0) {
- o = new MergeOption(name, parameters);
- } else
- if (name.compareTo("i") == 0) {
- o = new InvCheckCallOption(name, parameters);
- } else
- if (name.compareTo("w") == 0) {
- o = new WrapExceptionOption(name, parameters);
- } else
- if (name.compareTo("q") == 0) {
- o = new QuietOption(name, parameters);
- } else
- if (name.compareTo("a") == 0) {
- o = new AllOption(name, parameters);
- } else
- if (name.compareTo("x") == 0) {
- o = new XOption(name, parameters);
- } else
- if (name.compareTo("Z") == 0) {
- o = new Internal0Option(name, parameters);
- } else
- if (name.compareTo("j") == 0) {
- o = new NoInitialCompilationOption(name, parameters);
- } else {
- throw new RuntimeException("Java Contract Suite: error: unknown option -" + name);
- }
- }
- catch (NoClassDefFoundError _ex) {
- throw new RuntimeException("Attempt to perform in-process call to sun.tools.javac.Main failed because the class could not be found! In Java-2, make sure that the JDK's tools.jar (contain sun.tools.javac.*) is on your classpath!", _ex);
- }
- return o;
- }
-
- public TargetMetaclass newTarget(String name) {
- return new FileTarget(name);
- }
-
- public ArgMetaclassFactory() {
- }
-}
+
+public class ArgMetaclassFactory implements ParserMetaclassFactory
+{
+
+ public OptionMetaclass newOption(String name, Vector parameters)
+ {
+ OptionMetaclass o = null;
+ try
+ {
+ if (name.compareTo("h") == 0)
+ {
+ o = new HelpOption(name, parameters);
+ }
+ else if (name.compareTo("v") == 0)
+ {
+ o = new VerboseOption(name, parameters);
+ }
+ else if (name.compareTo("c") == 0)
+ {
+ o = new CompilerOption(name, parameters);
+ }
+ else if (name.compareTo("b") == 0)
+ {
+ o = new SourceCompilerOption(name, parameters);
+ }
+ else if (name.compareTo("n") == 0)
+ {
+ o = new NoRepositoryCompilationOption(name, parameters);
+ }
+ else if (name.compareTo("o") == 0)
+ {
+ o = new OutputOption(name, parameters);
+ }
+ else if (name.compareTo("y") == 0)
+ {
+ o = new OneOneOption(name, parameters);
+ }
+ else if (name.compareTo("k") == 0)
+ {
+ o = new RepositoryOutputOption(name, parameters);
+ }
+ else if (name.compareTo("d") == 0)
+ {
+ o = new DefaultExceptionOption(name, parameters);
+ }
+ else if (name.compareTo("r") == 0)
+ {
+ o = new CleanOption(name, parameters);
+ }
+ else if (name.compareTo("m") == 0)
+ {
+ o = new MergeOption(name, parameters);
+ }
+ else if (name.compareTo("i") == 0)
+ {
+ o = new InvCheckCallOption(name, parameters);
+ }
+ else if (name.compareTo("w") == 0)
+ {
+ o = new WrapExceptionOption(name, parameters);
+ }
+ else if (name.compareTo("q") == 0)
+ {
+ o = new QuietOption(name, parameters);
+ }
+ else if (name.compareTo("a") == 0)
+ {
+ o = new AllOption(name, parameters);
+ }
+ else if (name.compareTo("x") == 0)
+ {
+ o = new XOption(name, parameters);
+ }
+ else if (name.compareTo("Z") == 0)
+ {
+ o = new Internal0Option(name, parameters);
+ }
+ else if (name.compareTo("j") == 0)
+ {
+ o = new NoInitialCompilationOption(name, parameters);
+ }
+ else
+ {
+ throw new RuntimeException("Java Contract Suite: error: unknown option -" + name);
+ }
+ }
+ catch (NoClassDefFoundError _ex)
+ {
+ throw new RuntimeException(
+ "Attempt to perform in-process call to sun.tools.javac.Main failed because the class could not be found! In Java-2, make sure that the JDK's tools.jar (contain sun.tools.javac.*) is on your classpath!",
+ _ex);
+ }
+ return o;
+ }
+
+ public TargetMetaclass newTarget(String name)
+ {
+ return new FileTarget(name);
+ }
+
+ public ArgMetaclassFactory()
+ {
+ }
+}
Modified: trunk/source/java/net/sf/jcontracts/icontract/AssertionExpression.java
===================================================================
--- trunk/source/java/net/sf/jcontracts/icontract/AssertionExpression.java 2006-11-27 16:56:26 UTC (rev 33)
+++ trunk/source/java/net/sf/jcontracts/icontract/AssertionExpression.java 2006-11-27 20:14:50 UTC (rev 34)
@@ -8,865 +8,1149 @@
import org.apache.log4j.Logger;
-class AssertionExpression {
- private static final Logger log = Logger.getLogger(AssertionExpression.class);
- private String expression_;
- private IContracted subject_;
+class AssertionExpression
+{
+ private static final Logger log = Logger.getLogger(AssertionExpression.class);
- AssertionExpression(String expr, IContracted subject) {
- expression_ = expr.trim();
- subject_ = subject;
- }
+ private String expression_;
- void addBoundVariablesTo(Hashtable vartab) {
- String elementType = getElementType();
- String elementVar = getElementVar();
- vartab.put(elementVar, elementType);
- String quantifiedExpression = getQuantifiedExpression();
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- subassert.addBoundVariablesTo(vartab);
- }
- }
+ private IContracted subject_;
- boolean containsImplies(String expr) {
- return expr.indexOf("implies") != -1;
- }
+ AssertionExpression(String expr, IContracted subject)
+ {
+ expression_ = expr.trim();
+ subject_ = subject;
+ }
- String getCheckCode() {
- String code = "";
- String resultVar = "__result_" + getMangledValue(getElementVar());
- code = code + getPartialCheckCode();
- String prefix = getUpToQuantifier();
- code = code + "if (!" + prefix + resultVar + ")\n";
- return code;
- }
+ void addBoundVariablesTo(Hashtable vartab)
+ {
+ String elementType = getElementType();
+ String elementVar = getElementVar();
+ vartab.put(elementVar, elementType);
+ String quantifiedExpression = getQuantifiedExpression();
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ subassert.addBoundVariablesTo(vartab);
+ }
+ }
- private String getElementType() {
- int f = expression_.indexOf("forall ");
- if (f == -1) {
- f = expression_.indexOf("exists ");
- }
- int start = expression_.indexOf(" ", f);
- int end = expression_.indexOf(" ", start + 1);
- return expression_.substring(start, end).trim();
- }
+ boolean containsImplies(String expr)
+ {
+ return expr.indexOf("implies") != -1;
+ }
- private String getElementVar() {
- int dummy = 0;
- int start = 0;
- int end = 0;
- String res = "";
- try {
- int f = expression_.indexOf("forall ");
- if (f == -1) {
+ String getCheckCode()
+ {
+ String code = "";
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ code = code + getPartialCheckCode();
+ String prefix = getUpToQuantifier();
+ code = code + "if (!" + prefix + resultVar + ")\n";
+ return code;
+ }
+
+ private String getElementType()
+ {
+ int f = expression_.indexOf("forall ");
+ if (f == -1)
+ {
f = expression_.indexOf("exists ");
- }
- dummy = expression_.indexOf(" ", f);
- start = expression_.indexOf(" ", dummy + 1);
- end = expression_.indexOf(" ", start + 1);
- res = expression_.substring(start, end).trim();
- }
- catch (StringIndexOutOfBoundsException _ex) {
- throw new RuntimeException("can not determine the variable name in expression " + expression_);
- }
- return res;
- }
+ }
+ int start = expression_.indexOf(" ", f);
+ int end = expression_.indexOf(" ", start + 1);
+ return expression_.substring(start, end).trim();
+ }
- private String getExistsCheckCode() {
- String code = "";
- String quantificationDomain = getQuantificationDomain();
- if (isRangeDomain(quantificationDomain)) {
- code = getExistsCheckCode_OverRange();
- } else
- if (isArrayDomain()) {
- code = getExistsCheckCode_OverArray();
- } else
- if (isIteratorDomain()) {
- code = getExistsCheckCode_OverIterator(false);
- } else
- if (isEnumerationDomain()) {
- code = getExistsCheckCode_OverEnumeration(false);
- } else {
- String d = getQuantificationDomain().trim();
- String type_of_domain = "";
- try {
- type_of_domain = subject_.getTypeOfValue(d).trim();
- if (type_of_domain.indexOf("[") != -1) {
- code = getExistsCheckCode_OverArray();
- } else
- if (type_of_domain.equals("java.util.Enumeration")) {
- code = getExistsCheckCode_OverEnumeration(false);
- } else
- if (type_of_domain.equals("java.util.Iterator")) {
- code = getExistsCheckCode_OverIterator(false);
- } else
- if (isImplementationOf("java.util.Iterator", type_of_domain)) {
- code = getExistsCheckCode_OverIterator(false);
- } else
- if (isImplementationOf("java.util.Enumeration", type_of_domain)) {
- code = getExistsCheckCode_OverEnumeration(false);
- } else
- if (hasImplementationOfMethod("elements", "java.util.Enumeration", type_of_domain)) {
- code = getExistsCheckCode_OverEnumeration(true);
- } else
- if (hasImplementationOfMethod("iterator", "java.util.Iterator", type_of_domain)) {
- code = getExistsCheckCode_OverIterator(true);
- } else {
- String dd = getQuantificationDomain().trim();
- log.warn("The type of " + dd + " in " + ((CodeMetaclass)subject_).getSignature() + " is " + type_of_domain + "\n" + "Complete assertion: " + subject_ + "\nQuantifier domains must be: Array, Range (e.g. a .. b [by c]), Enumeration, Iterator or implementation thereof or\nimplementors of 'Enumeration elements()' or 'Iterator iterator()' (e.g. the Java 2 Collections, JDK 1.1 Vector, etc.)\n" + "As a best effort will use java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
- code = getExistsCheckCode_OverEnumeration(false);
+ private String getElementVar()
+ {
+ int dummy = 0;
+ int start = 0;
+ int end = 0;
+ String res = "";
+ try
+ {
+ int f = expression_.indexOf("forall ");
+ if (f == -1)
+ {
+ f = expression_.indexOf("exists ");
}
- }
- catch (UnableToDetermineTypeException e) {
- String dd = getQuantificationDomain().trim();
- log.warn("Could not determine type of " + dd + " in " + ((CodeMetaclass)subject_).getSignature() + "\n" + "Complete assertion: " + subject_ + "\n" + "Using java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
- log.warn(e.getMessage());
+ dummy = expression_.indexOf(" ", f);
+ start = expression_.indexOf(" ", dummy + 1);
+ end = expression_.indexOf(" ", start + 1);
+ res = expression_.substring(start, end).trim();
+ }
+ catch (StringIndexOutOfBoundsException _ex)
+ {
+ throw new RuntimeException("can not determine the variable name in expression " + expression_);
+ }
+ return res;
+ }
+
+ private String getExistsCheckCode()
+ {
+ String code = "";
+ String quantificationDomain = getQuantificationDomain();
+ if (isRangeDomain(quantificationDomain))
+ {
+ code = getExistsCheckCode_OverRange();
+ }
+ else if (isArrayDomain())
+ {
+ code = getExistsCheckCode_OverArray();
+ }
+ else if (isIteratorDomain())
+ {
+ code = getExistsCheckCode_OverIterator(false);
+ }
+ else if (isEnumerationDomain())
+ {
code = getExistsCheckCode_OverEnumeration(false);
- }
- }
- return code;
- }
+ }
+ else
+ {
+ String d = getQuantificationDomain().trim();
+ String type_of_domain = "";
+ try
+ {
+ type_of_domain = subject_.getTypeOfValue(d).trim();
+ if (type_of_domain.indexOf("[") != -1)
+ {
+ code = getExistsCheckCode_OverArray();
+ }
+ else if (type_of_domain.equals("java.util.Enumeration"))
+ {
+ code = getExistsCheckCode_OverEnumeration(false);
+ }
+ else if (type_of_domain.equals("java.util.Iterator"))
+ {
+ code = getExistsCheckCode_OverIterator(false);
+ }
+ else if (isImplementationOf("java.util.Iterator", type_of_domain))
+ {
+ code = getExistsCheckCode_OverIterator(false);
+ }
+ else if (isImplementationOf("java.util.Enumeration", type_of_domain))
+ {
+ code = getExistsCheckCode_OverEnumeration(false);
+ }
+ else if (hasImplementationOfMethod("elements", "java.util.Enumeration", type_of_domain))
+ {
+ code = getExistsCheckCode_OverEnumeration(true);
+ }
+ else if (hasImplementationOfMethod("iterator", "java.util.Iterator", type_of_domain))
+ {
+ code = getExistsCheckCode_OverIterator(true);
+ }
+ else
+ {
+ String dd = getQuantificationDomain().trim();
+ log
+ .warn("The type of "
+ + dd
+ + " in "
+ + ((CodeMetaclass) subject_).getSignature()
+ + " is "
+ + type_of_domain
+ + "\n"
+ + "Complete assertion: "
+ + subject_
+ + "\nQuantifier domains must be: Array, Range (e.g. a .. b [by c]), Enumeration, Iterator or implementation thereof or\nimplementors of 'Enumeration elements()' or 'Iterator iterator()' (e.g. the Java 2 Collections, JDK 1.1 Vector, etc.)\n"
+ + "As a best effort will use java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
+ code = getExistsCheckCode_OverEnumeration(false);
+ }
+ }
+ catch (UnableToDetermineTypeException e)
+ {
+ String dd = getQuantificationDomain().trim();
+ log
+ .warn("Could not determine type of "
+ + dd
+ + " in "
+ + ((CodeMetaclass) subject_).getSignature()
+ + "\n"
+ + "Complete assertion: "
+ + subject_
+ + "\n"
+ + "Using java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
+ log.warn(e.getMessage());
+ code = getExistsCheckCode_OverEnumeration(false);
+ }
+ }
+ return code;
+ }
- private String getExistsCheckCode_OverArray() {
- String code = "";
- String elementType = getElementType();
- String elementVar = getElementVar();
- String indexVar = "__index_" + getMangledValue(getElementVar());
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=false;\n";
- code = code + "for ( int " + indexVar + "= 0; (" + indexVar + " < " + quantificationDomain + ".length) && !" + resultVar + "; " + indexVar + "++){\n";
- code = code + " " + elementType + " " + elementVar + "= " + quantificationDomain + "[" + indexVar + "];\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // amount to dc\n";
- code = code + "else {\n";
- code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
- }
- code = code + "} // loop\n";
- return code;
- }
+ private String getExistsCheckCode_OverArray()
+ {
+ String code = "";
+ String elementType = getElementType();
+ String elementVar = getElementVar();
+ String indexVar = "__index_" + getMangledValue(getElementVar());
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=false;\n";
+ code = code + "for ( int " + indexVar + "= 0; (" + indexVar + " < " + quantificationDomain + ".length) && !"
+ + resultVar + "; " + indexVar + "++){\n";
+ code = code + " " + elementType + " " + elementVar + "= " + quantificationDomain + "[" + indexVar + "];\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // amount to dc\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
+ }
+ code = code + "} // loop\n";
+ return code;
+ }
- private String getExistsCheckCode_OverEnumeration(boolean enumerationImpl) {
- String code = "";
- String elementType = getElementType();
- String castElementType = elementType;
- if (elementType.equals("int")) {
- castElementType = "Integer";
- }
- if (elementType.equals("float")) {
- castElementType = "Float";
- }
- if (elementType.equals("boolean")) {
- castElementType = "Boolean";
- }
- if (elementType.equals("byte")) {
- castElementType = "Byte";
- }
- if (elementType.equals("double")) {
- castElementType = "Double";
- }
- if (elementType.equals("long")) {
- castElementType = "Long";
- }
- if (elementType.equals("short")) {
- castElementType = "Short";
- }
- if (elementType.equals("char")) {
- castElementType = "Character";
- }
- String enumVar = "__" + getMangledValue(getElementVar()) + "_enum";
- String elementVar = getElementVar();
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=false;\n";
- String postfix = "";
- if (enumerationImpl) {
- postfix = ".elements()";
- }
- code = code + "for (java.util.Enumeration " + enumVar + "=" + quantificationDomain + postfix + ";\n";
- code = code + " " + enumVar + ".hasMoreElements() && !" + resultVar + "; ){\n";
- code = code + " " + castElementType + " " + elementVar + "=(";
- code = code + castElementType + ")(" + enumVar + ".nextElement());\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // amount to dc\n";
- code = code + "else {\n";
- code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
- }
- code = code + "} // loop\n";
- return code;
- }
+ private String getExistsCheckCode_OverEnumeration(boolean enumerationImpl)
+ {
+ String code = "";
+ String elementType = getElementType();
+ String castElementType = elementType;
+ if (elementType.equals("int"))
+ {
+ castElementType = "Integer";
+ }
+ if (elementType.equals("float"))
+ {
+ castElementType = "Float";
+ }
+ if (elementType.equals("boolean"))
+ {
+ castElementType = "Boolean";
+ }
+ if (elementType.equals("byte"))
+ {
+ castElementType = "Byte";
+ }
+ if (elementType.equals("double"))
+ {
+ castElementType = "Double";
+ }
+ if (elementType.equals("long"))
+ {
+ castElementType = "Long";
+ }
+ if (elementType.equals("short"))
+ {
+ castElementType = "Short";
+ }
+ if (elementType.equals("char"))
+ {
+ castElementType = "Character";
+ }
+ String enumVar = "__" + getMangledValue(getElementVar()) + "_enum";
+ String elementVar = getElementVar();
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=false;\n";
+ String postfix = "";
+ if (enumerationImpl)
+ {
+ postfix = ".elements()";
+ }
+ code = code + "for (java.util.Enumeration " + enumVar + "=" + quantificationDomain + postfix + ";\n";
+ code = code + " " + enumVar + ".hasMoreElements() && !" + resultVar + "; ){\n";
+ code = code + " " + castElementType + " " + elementVar + "=(";
+ code = code + castElementType + ")(" + enumVar + ".nextElement());\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // amount to dc\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
+ }
+ code = code + "} // loop\n";
+ return code;
+ }
- private String getExistsCheckCode_OverIterator(boolean iteratorImpl) {
- String code = "";
- String elementType = getElementType();
- String castElementType = elementType;
- if (elementType.equals("int")) {
- castElementType = "Integer";
- }
- if (elementType.equals("float")) {
- castElementType = "Float";
- }
- if (elementType.equals("boolean")) {
- castElementType = "Boolean";
- }
- if (elementType.equals("byte")) {
- castElementType = "Byte";
- }
- if (elementType.equals("double")) {
- castElementType = "Double";
- }
- if (elementType.equals("long")) {
- castElementType = "Long";
- }
- if (elementType.equals("short")) {
- castElementType = "Short";
- }
- if (elementType.equals("char")) {
- castElementType = "Character";
- }
- String enumVar = "__" + getMangledValue(getElementVar()) + "_iterator";
- String elementVar = getElementVar();
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=false;\n";
- String postfix = "";
- if (iteratorImpl) {
- postfix = ".iterator()";
- }
- code = code + "for (java.util.Iterator " + enumVar + "=" + quantificationDomain + postfix + ";\n";
- code = code + " " + enumVar + ".hasNext() && !" + resultVar + "; ){\n";
- code = code + " " + castElementType + " " + elementVar + "=(";
- code = code + castElementType + ")(" + enumVar + ".next());\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // amount to dc\n";
- code = code + "else {\n";
- code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
- }
- code = code + "} // loop\n";
- return code;
- }
+ private String getExistsCheckCode_OverIterator(boolean iteratorImpl)
+ {
+ String code = "";
+ String elementType = getElementType();
+ String castElementType = elementType;
+ if (elementType.equals("int"))
+ {
+ castElementType = "Integer";
+ }
+ if (elementType.equals("float"))
+ {
+ castElementType = "Float";
+ }
+ if (elementType.equals("boolean"))
+ {
+ castElementType = "Boolean";
+ }
+ if (elementType.equals("byte"))
+ {
+ castElementType = "Byte";
+ }
+ if (elementType.equals("double"))
+ {
+ castElementType = "Double";
+ }
+ if (elementType.equals("long"))
+ {
+ castElementType = "Long";
+ }
+ if (elementType.equals("short"))
+ {
+ castElementType = "Short";
+ }
+ if (elementType.equals("char"))
+ {
+ castElementType = "Character";
+ }
+ String enumVar = "__" + getMangledValue(getElementVar()) + "_iterator";
+ String elementVar = getElementVar();
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=false;\n";
+ String postfix = "";
+ if (iteratorImpl)
+ {
+ postfix = ".iterator()";
+ }
+ code = code + "for (java.util.Iterator " + enumVar + "=" + quantificationDomain + postfix + ";\n";
+ code = code + " " + enumVar + ".hasNext() && !" + resultVar + "; ){\n";
+ code = code + " " + castElementType + " " + elementVar + "=(";
+ code = code + castElementType + ")(" + enumVar + ".next());\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // amount to dc\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
+ }
+ code = code + "} // loop\n";
+ return code;
+ }
- private String getExistsCheckCode_OverRange() {
- String code = "";
- String elementType = getElementType();
- String _tmp = "__" + getMangledValue(getElementVar()) + "_counter";
- String elementVar = getElementVar();
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String rangeStart = getRangeStart(quantificationDomain);
- String rangeEnd = getRangeEnd(quantificationDomain);
- String step = getRangeStep(quantificationDomain);
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=false;\n";
- code = code + "for (" + elementType + " " + elementVar + "=" + rangeStart + "; ";
- String compare = "";
- if (step.startsWith("-")) {
- compare = " >= ";
- } else {
- compare = " <= ";
- }
- code = code + "(" + elementVar + compare + rangeEnd + ") && !" + resultVar + "; " + elementVar + "=" + elementVar + "+(" + elementType + ")" + step + " ){\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // amount to dc\n";
- code = code + "else {\n";
- code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
- }
- code = code + "} // loop\n";
- return code;
- }
+ private String getExistsCheckCode_OverRange()
+ {
+ String code = "";
+ String elementType = getElementType();
+ String _tmp = "__" + getMangledValue(getElementVar()) + "_counter";
+ String elementVar = getElementVar();
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String rangeStart = getRangeStart(quantificationDomain);
+ String rangeEnd = getRangeEnd(quantificationDomain);
+ String step = getRangeStep(quantificationDomain);
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=false;\n";
+ code = code + "for (" + elementType + " " + elementVar + "=" + rangeStart + "; ";
+ String compare = "";
+ if (step.startsWith("-"))
+ {
+ compare = " >= ";
+ }
+ else
+ {
+ compare = " <= ";
+ }
+ code = code + "(" + elementVar + compare + rangeEnd + ") && !" + resultVar + "; " + elementVar + "="
+ + elementVar + "+(" + elementType + ")" + step + " ){\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // amount to dc\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + " = " + getImplication(quantifiedExpression) + "; // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + quantifiedExpression + ";\n";
+ }
+ code = code + "} // loop\n";
+ return code;
+ }
- private String getForallCheckCode() {
- String code = "";
- String quantificationDomain = getQuantificationDomain();
- if (isRangeDomain(quantificationDomain)) {
- code = getForallCheckCode_OverRange();
- } else
- if (isArrayDomain()) {
- code = getForallCheckCode_OverArray();
- } else
- if (isIteratorDomain()) {
- code = getForallCheckCode_OverIterator(false);
- } else
- if (isEnumerationDomain()) {
- code = getForallCheckCode_OverEnumeration(false);
- } else {
- String d = getQuantificationDomain().trim();
- String type_of_domain = "";
- try {
- type_of_domain = subject_.getTypeOfValue(d).trim();
- if (type_of_domain.indexOf("[") != -1) {
- code = getForallCheckCode_OverArray();
- } else
- if (type_of_domain.equals("java.util.Enumeration")) {
- code = getForallCheckCode_OverEnumeration(false);
- } else
- if (type_of_domain.equals("java.util.Iterator")) {
- code = getForallCheckCode_OverIterator(false);
- } else
- if (isImplementationOf("java.util.Iterator", type_of_domain)) {
- code = getForallCheckCode_OverIterator(false);
- } else
- if (isImplementationOf("java.util.Enumeration", type_of_domain)) {
- code = getForallCheckCode_OverEnumeration(false);
- } else
- if (hasImplementationOfMethod("elements", "java.util.Enumeration", type_of_domain)) {
- code = getForallCheckCode_OverEnumeration(true);
- } else
- if (hasImplementationOfMethod("iterator", "java.util.Iterator", type_of_domain)) {
- code = getForallCheckCode_OverIterator(true);
- } else {
- String dd = getQuantificationDomain().trim();
- log.warn("The type of " + dd + " in " + ((CodeMetaclass)subject_).getSignature() + " is " + type_of_domain + "\n" + "Complete assertion: " + subject_ + "\nQuantifier domains must be: Array, Range (e.g. a .. b [by c]), Enumeration, Iterator or implementation thereof or\nimplementors of 'Enumeration elements()' or 'Iterator iterator()' (e.g. the Java 2 Collections, JDK 1.1 Vector, etc.)\n" + "As a best effort will use java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
- code = getForallCheckCode_OverEnumeration(false);
+ private String getForallCheckCode()
+ {
+ String code = "";
+ String quantificationDomain = getQuantificationDomain();
+ if (isRangeDomain(quantificationDomain))
+ {
+ code = getForallCheckCode_OverRange();
+ }
+ else if (isArrayDomain())
+ {
+ code = getForallCheckCode_OverArray();
+ }
+ else if (isIteratorDomain())
+ {
+ code = getForallCheckCode_OverIterator(false);
+ }
+ else if (isEnumerationDomain())
+ {
+ code = getForallCheckCode_OverEnumeration(false);
+ }
+ else
+ {
+ String d = getQuantificationDomain().trim();
+ String type_of_domain = "";
+ try
+ {
+ type_of_domain = subject_.getTypeOfValue(d).trim();
+ if (type_of_domain.indexOf("[") != -1)
+ {
+ code = getForallCheckCode_OverArray();
+ }
+ else if (type_of_domain.equals("java.util.Enumeration"))
+ {
+ code = getForallCheckCode_OverEnumeration(false);
+ }
+ else if (type_of_domain.equals("java.util.Iterator"))
+ {
+ code = getForallCheckCode_OverIterator(false);
+ }
+ else if (isImplementationOf("java.util.Iterator", type_of_domain))
+ {
+ code = getForallCheckCode_OverIterator(false);
+ }
+ else if (isImplementationOf("java.util.Enumeration", type_of_domain))
+ {
+ code = getForallCheckCode_OverEnumeration(false);
+ }
+ else if (hasImplementationOfMethod("elements", "java.util.Enumeration", type_of_domain))
+ {
+ code = getForallCheckCode_OverEnumeration(true);
+ }
+ else if (hasImplementationOfMethod("iterator", "java.util.Iterator", type_of_domain))
+ {
+ code = getForallCheckCode_OverIterator(true);
+ }
+ else
+ {
+ String dd = getQuantificationDomain().trim();
+ log
+ .warn("The type of "
+ + dd
+ + " in "
+ + ((CodeMetaclass) subject_).getSignature()
+ + " is "
+ + type_of_domain
+ + "\n"
+ + "Complete assertion: "
+ + subject_
+ + "\nQuantifier domains must be: Array, Range (e.g. a .. b [by c]), Enumeration, Iterator or implementation thereof or\nimplementors of 'Enumeration elements()' or 'Iterator iterator()' (e.g. the Java 2 Collections, JDK 1.1 Vector, etc.)\n"
+ + "As a best effort will use java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
+ code = getForallCheckCode_OverEnumeration(false);
+ }
}
- }
- catch (UnableToDetermineTypeException e) {
- String dd = getQuantificationDomain().trim();
- log.warn("Could not determine type of " + dd + " in " + ((CodeMetaclass)subject_).getSignature() + "\n" + "Complete assertion: " + subject_ + "\n" + "Using java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
- log.warn(e.getMessage());
- code = getForallCheckCode_OverEnumeration(false);
- }
- }
- return code;
- }
+ catch (UnableToDetermineTypeException e)
+ {
+ String dd = getQuantificationDomain().trim();
+ log
+ .warn("Could not determine type of "
+ + dd
+ + " in "
+ + ((CodeMetaclass) subject_).getSignature()
+ + "\n"
+ + "Complete assertion: "
+ + subject_
+ + "\n"
+ + "Using java.util.Enumeration by default. Use '.. inarray ..', '.. inrange ..' or '.. initerator ..' instead of '.. in ..' if required as a workaround.");
+ log.warn(e.getMessage());
+ code = getForallCheckCode_OverEnumeration(false);
+ }
+ }
+ return code;
+ }
- private String getForallCheckCode_OverArray() {
- String code = "";
- String elementType = getElementType();
- String elementVar = getElementVar();
- String indexVar = "__index_" + getMangledValue(getElementVar());
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=true;\n";
- code = code + "for ( int " + indexVar + "= 0; " + indexVar + " < " + quantificationDomain + ".length; " + indexVar + "++){\n";
- code = code + " " + elementType + " " + elementVar + "= " + quantificationDomain + "[" + indexVar + "];\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + resultVar + " && " + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // implication evaluates to true, does not affect return\n";
- code = code + "else {\n";
- code = code + " " + resultVar + "=" + resultVar + " && (" + getImplication(quantifiedExpression) + " ); // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + resultVar + " && (" + quantifiedExpression + ");\n";
- }
- code = code + "}\n";
- return code;
- }
+ private String getForallCheckCode_OverArray()
+ {
+ String code = "";
+ String elementType = getElementType();
+ String elementVar = getElementVar();
+ String indexVar = "__index_" + getMangledValue(getElementVar());
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=true;\n";
+ code = code + "for ( int " + indexVar + "= 0; " + indexVar + " < " + quantificationDomain + ".length; "
+ + indexVar + "++){\n";
+ code = code + " " + elementType + " " + elementVar + "= " + quantificationDomain + "[" + indexVar + "];\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + resultVar + " && " + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // implication evaluates to true, does not affect return\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + "=" + resultVar + " && (" + getImplication(quantifiedExpression)
+ + " ); // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + resultVar + " && (" + quantifiedExpression + ");\n";
+ }
+ code = code + "}\n";
+ return code;
+ }
- private String getForallCheckCode_OverEnumeration(boolean enumerationImpl) {
- String code = "";
- String elementType = getElementType();
- String castElementType = elementType;
- if (elementType.equals("int")) {
- castElementType = "Integer";
- }
- if (elementType.equals("float")) {
- castElementType = "Float";
- }
- if (elementType.equals("boolean")) {
- castElementType = "Boolean";
- }
- if (elementType.equals("byte")) {
- castElementType = "Byte";
- }
- if (elementType.equals("double")) {
- castElementType = "Double";
- }
- if (elementType.equals("long")) {
- castElementType = "Long";
- }
- if (elementType.equals("short")) {
- castElementType = "Short";
- }
- if (elementType.equals("char")) {
- castElementType = "Character";
- }
- String enumVar = "__" + getMangledValue(getElementVar()) + "_enum";
- String elementVar = getElementVar();
- String resultVar = "__result_" + getMangledValue(getElementVar());
- String quantificationDomain = getQuantificationDomain();
- String quantifiedExpression = getQuantifiedExpression();
- code = code + "boolean " + resultVar + "=true;\n";
- String postfix = "";
- if (enumerationImpl) {
- postfix = ".elements()";
- }
- code = code + "for (java.util.Enumeration " + enumVar + "=" + quantificationDomain + postfix + ";\n";
- code = code + " " + enumVar + ".hasMoreElements() && " + resultVar + "; ){\n";
- code = code + " " + castElementType + " " + elementVar + "=(";
- code = code + castElementType + ")(" + enumVar + ".nextElement());\n";
- AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
- if (subassert.includesQuantifier()) {
- code = code + subassert.getPartialCheckCode();
- String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
- code = code + resultVar + "=" + resultVar + " && " + subresultVar + ";\n";
- } else
- if (containsImplies(quantifiedExpression)) {
- code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression) + " )) // implication condition\n";
- code = code + " { } // implication evaluates to true, does not affect return\n";
- code = code + "else {\n";
- code = code + " " + resultVar + "=" + resultVar + " && (" + getImplication(quantifiedExpression) + " ); // the implication \n";
- code = code + "}\n";
- } else {
- code = code + " " + resultVar + "=" + resultVar + " && (" + quantifiedExpression + ");\n";
- }
- code = code + "}\n";
- return code;
- }
+ private String getForallCheckCode_OverEnumeration(boolean enumerationImpl)
+ {
+ String code = "";
+ String elementType = getElementType();
+ String castElementType = elementType;
+ if (elementType.equals("int"))
+ {
+ castElementType = "Integer";
+ }
+ if (elementType.equals("float"))
+ {
+ castElementType = "Float";
+ }
+ if (elementType.equals("boolean"))
+ {
+ castElementType = "Boolean";
+ }
+ if (elementType.equals("byte"))
+ {
+ castElementType = "Byte";
+ }
+ if (elementType.equals("double"))
+ {
+ castElementType = "Double";
+ }
+ if (elementType.equals("long"))
+ {
+ castElementType = "Long";
+ }
+ if (elementType.equals("short"))
+ {
+ castElementType = "Short";
+ }
+ if (elementType.equals("char"))
+ {
+ castElementType = "Character";
+ }
+ String enumVar = "__" + getMangledValue(getElementVar()) + "_enum";
+ String elementVar = getElementVar();
+ String resultVar = "__result_" + getMangledValue(getElementVar());
+ String quantificationDomain = getQuantificationDomain();
+ String quantifiedExpression = getQuantifiedExpression();
+ code = code + "boolean " + resultVar + "=true;\n";
+ String postfix = "";
+ if (enumerationImpl)
+ {
+ postfix = ".elements()";
+ }
+ code = code + "for (java.util.Enumeration " + enumVar + "=" + quantificationDomain + postfix + ";\n";
+ code = code + " " + enumVar + ".hasMoreElements() && " + resultVar + "; ){\n";
+ code = code + " " + castElementType + " " + elementVar + "=(";
+ code = code + castElementType + ")(" + enumVar + ".nextElement());\n";
+ AssertionExpression subassert = new AssertionExpression(quantifiedExpression, subject_);
+ if (subassert.includesQuantifier())
+ {
+ code = code + subassert.getPartialCheckCode();
+ String subresultVar = "__result_" + getMangledValue(subassert.getElementVar());
+ code = code + resultVar + "=" + resultVar + " && " + subresultVar + ";\n";
+ }
+ else if (containsImplies(quantifiedExpression))
+ {
+ code = code + "if (!( " + getImpliesConditionExpression(quantifiedExpression)
+ + " )) // implication condition\n";
+ code = code + " { } // implication evaluates to true, does not affect return\n";
+ code = code + "else {\n";
+ code = code + " " + resultVar + "=" + resultVar + " && (" + getImplication(quantifiedExpression)
+ + " ); // the implication \n";
+ code = code + "}\n";
+ }
+ else
+ {
+ code = code + " " + resultVar + "=" + resultVar + " && (" + quantifiedExpression + ");\n";
+ }
+ code = code + "}\n";
+ return code;
+ }
- private String getForallCheckCode_OverIterator(boolean iteratorImpl) {
- String code = "";
- String elementType = getElementType();
- String castElementType = elementType;
- if (elementType.equals("int")) {
- castElementType = "Integer";
- }
- if (elementType.equals("float")) {
- castElementType = "Float";
- }
- if (elementType.equals("boolean")) {
- castElementType = "Boolean";
- }
- if (elementType.equals("byte")) {
- castElementType = "Byte";
- }
- if (elementType.equals("double")) {
- castElementType = "Double";
- }
- if (elementType.equals("long")) {
- castElementType = "Long";
- }
- if (elementType.equals("short")) {
- castElementType = "Short";
- }
- if (elementType.equals("char")) {
- castEleme...
[truncated message content] |
