From cbef025f838faf6798f240872e56426cc8ce83b5 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 13 Jan 2020 15:18:38 +0100
Subject: [PATCH] Fix Javadoc problems
* Removed Javadoc comments that were basically empty
(they only contained the blank template generated by the IDE, which
was never filled out and in most cases outdated)
* Removed incorrectly placed Javadoc comments with only an @author line
(Git tracks authorship anyway)
* Fixed some HTML syntax errors in Javadoc comments
* Changed some comments' ASCII art so they are not incorrectly
considered Javadoc comments
---
src/main/java/de/tla2b/TLA2B.java | 4 -
.../java/de/tla2b/analysis/BOperation.java | 10 --
.../analysis/InstanceTransformation.java | 41 -----
.../de/tla2b/analysis/RecursiveFunktion.java | 4 -
.../java/de/tla2b/analysis/SpecAnalyser.java | 4 -
.../java/de/tla2b/analysis/SymbolRenamer.java | 8 -
.../java/de/tla2b/analysis/SymbolSorter.java | 6 +-
.../java/de/tla2b/analysis/TypeChecker.java | 143 ++++++------------
.../de/tla2b/config/ConfigfileEvaluator.java | 17 +--
.../java/de/tla2b/config/ModuleOverrider.java | 18 ---
.../java/de/tla2b/config/TLCValueNode.java | 9 --
src/main/java/de/tla2b/config/ValueObj.java | 4 -
.../exceptions/SemanticErrorException.java | 4 -
.../exceptions/UnificationException.java | 4 -
.../de/tla2b/global/TranslationGlobals.java | 4 -
src/main/java/de/tla2b/types/EnumType.java | 8 +-
src/main/java/de/tla2b/types/StringType.java | 4 -
.../de/tla2b/types/StructOrFunctionType.java | 4 -
src/main/java/de/tla2bAst/BAstCreator.java | 15 +-
.../de/tla2bAst/ExpressionTranslator.java | 8 -
src/main/java/de/tla2bAst/Translator.java | 6 -
.../expression/ComplexExpressionTest.java | 4 -
.../expression/SimpleExpressionTest.java | 4 -
.../java/de/tla2b/expression/TestError.java | 4 -
.../de/tla2b/expression/TestKeywords.java | 4 -
.../de/tla2b/expression/TestSequences.java | 4 -
.../de/tla2b/prettyprintb/BBuiltInsTest.java | 4 -
.../de/tla2b/prettyprintb/FunctionTest.java | 12 +-
.../prettyprintb/LogicOperatorsTest.java | 22 ++-
.../de/tla2b/prettyprintb/PrecedenceTest.java | 4 -
.../de/tla2b/prettyprintb/RecordTest.java | 24 ++-
.../java/de/tla2b/prettyprintb/SetsTest.java | 28 ++--
.../java/de/tla2b/prettyprintb/TupleTest.java | 4 -
.../de/tla2b/prettyprintb/VariablesTest.java | 4 -
.../standardmodules/ModuleFiniteSetsTest.java | 4 -
.../standardmodules/ModuleNaturalsTest.java | 16 +-
.../de/tla2b/typechecking/BBuiltInsTest.java | 16 +-
.../de/tla2b/typechecking/ConfigTest.java | 4 -
.../tla2b/typechecking/ConstantTypesTest.java | 4 -
.../tla2b/typechecking/DefinitionsTest.java | 12 +-
.../de/tla2b/typechecking/ExceptTest.java | 4 -
.../de/tla2b/typechecking/ExtendsTest.java | 4 -
.../de/tla2b/typechecking/FunctionTest.java | 32 ++--
.../de/tla2b/typechecking/InstanceTest.java | 4 -
.../typechecking/LogicOperatorsTest.java | 16 +-
.../MiscellaneousConstructsTest.java | 16 +-
.../java/de/tla2b/typechecking/OpArgTest.java | 4 -
.../java/de/tla2b/typechecking/SetTest.java | 40 ++---
.../de/tla2b/typechecking/StringTest.java | 12 +-
.../de/tla2b/typechecking/StructTest.java | 24 ++-
.../java/de/tla2b/typechecking/TupleTest.java | 4 +-
.../tla2b/typechecking/TypeConflictsTest.java | 4 -
.../standardmodules/TestModuleFiniteSets.java | 12 +-
.../standardmodules/TestModuleIntegers.java | 12 +-
.../standardmodules/TestModuleNaturals.java | 20 +--
.../standardmodules/TestModuleSequences.java | 32 ++--
.../java/de/tla2b/util/TestTypeChecker.java | 4 -
src/test/java/de/tla2b/util/TestUtil.java | 4 -
58 files changed, 198 insertions(+), 553 deletions(-)
diff --git a/src/main/java/de/tla2b/TLA2B.java b/src/main/java/de/tla2b/TLA2B.java
index 31562e5..7848c35 100644
--- a/src/main/java/de/tla2b/TLA2B.java
+++ b/src/main/java/de/tla2b/TLA2B.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b;
import org.apache.commons.cli.CommandLine;
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 447ab98..91dd132 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import java.util.ArrayList;
@@ -321,9 +317,6 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
findUnchangedVaribalesInSemanticNode(node);
}
- /**
- * @param node2
- */
private void findUnchangedVaribalesInSemanticNode(SemanticNode node) {
switch (node.getKind()) {
case OpApplKind: {
@@ -344,9 +337,6 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
}
- /**
- * @param node2
- */
private void findUnchangedVariablesInOpApplNode(OpApplNode n) {
int kind = n.getOperator().getKind();
diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index e8ab4c5..2d0b92b 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import java.util.Hashtable;
@@ -34,9 +30,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
private int substitutionId = 11;
- /**
- * @param moduleNode
- */
public InstanceTransformation(ModuleNode moduleNode) {
defs = moduleNode.getOpDefs();
defsHash = new Hashtable<String, OpDefNode>();
@@ -70,12 +63,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
}
- /**
- * @param exprOrOpArgNode
- * @param prefix
- * @return
- * @throws AbortException
- */
private ExprOrOpArgNode generateNewExprOrOpArgNode(ExprOrOpArgNode n,
String prefix) throws AbortException {
if (n instanceof ExprNode) {
@@ -85,12 +72,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
}
- /**
- * @param body
- * @param prefix
- * @return
- * @throws AbortException
- */
private ExprNode generateNewExprNode(ExprNode n, String prefix)
throws AbortException {
switch (n.getKind()) {
@@ -158,12 +139,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
throw new RuntimeException();
}
- /**
- * @param n
- * @param prefix
- * @return
- * @throws AbortException
- */
private ExprNode generateNewOpApplNode(OpApplNode n, String prefix)
throws AbortException {
switch (n.getOperator().getKind()) {
@@ -232,12 +207,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
throw new RuntimeException("OpApplkind not implemented jet");
}
- /**
- * @param n
- * @param prefix
- * @return
- * @throws AbortException
- */
private ExprNode generateNewBuiltInNode(OpApplNode n, String prefix)
throws AbortException {
switch (getOpCode(n.getOperator().getName())) {
@@ -324,12 +293,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
}
- /**
- * @param args
- * @param prefix
- * @return
- * @throws AbortException
- */
private ExprOrOpArgNode[] generateNewArgs(ExprOrOpArgNode[] args,
String prefix) throws AbortException {
ExprOrOpArgNode[] res = new ExprOrOpArgNode[args.length];
@@ -339,10 +302,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
return res;
}
- /**
- * @param oldParams
- * @return
- */
private FormalParamNode[] generateNewParams(FormalParamNode[] oldParams) {
FormalParamNode[] newParams = new FormalParamNode[oldParams.length];
for (int i = 0; i < oldParams.length; i++) {
diff --git a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
index 54ccc54..97c9bfc 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import de.tla2b.exceptions.NotImplementedException;
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 6d04504..2bb8065 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import java.util.ArrayList;
diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index 0471c86..50267aa 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
@@ -123,10 +119,6 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
private Set<String> globalNames = new HashSet<String>();
private Hashtable<OpDefNode, Set<String>> usedNamesTable = new Hashtable<OpDefNode, Set<String>>();
- /**
- * @param moduleNode
- * @param specAnalyser
- */
public SymbolRenamer(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
this.usedDefinitions = specAnalyser.getUsedDefinitions();
diff --git a/src/main/java/de/tla2b/analysis/SymbolSorter.java b/src/main/java/de/tla2b/analysis/SymbolSorter.java
index 514837f..f32ed64 100644
--- a/src/main/java/de/tla2b/analysis/SymbolSorter.java
+++ b/src/main/java/de/tla2b/analysis/SymbolSorter.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import java.util.Arrays;
@@ -80,4 +76,4 @@ class OpDefNodeComparator implements Comparator<OpDefNode> {
return 1;
return 0;
}
-}
\ No newline at end of file
+}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 70120d2..5e92c53 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import java.util.ArrayList;
@@ -63,11 +59,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
private ConfigfileEvaluator conEval;
- /**
- * @param moduleNode
- * @param conEval
- * @param specAnalyser
- */
public TypeChecker(ModuleNode moduleNode, ConfigfileEvaluator conEval, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
this.specAnalyser = specAnalyser;
@@ -221,10 +212,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
- /**
- * @param def
- * @throws TLA2BException
- */
public void visitOpDefNode(OpDefNode def) throws TLA2BException {
FormalParamNode[] params = def.getParams();
for (int i = 0; i < params.length; i++) {
@@ -254,12 +241,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
}
- /**
- * @param exprOrOpArgNode
- * @param instance
- * @throws TypeErrorException
- * @throws NotImplementedException
- */
private TLAType visitExprOrOpArgNode(ExprOrOpArgNode n, TLAType expected) throws TLA2BException {
if (n instanceof ExprNode) {
return visitExprNode((ExprNode) n, expected);
@@ -351,12 +332,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return (TLAType) n.getToolObject(TYPE_ID);
}
- /**
- * @param n
- * @param expected
- * @return {@link TLAType}
- * @throws TLA2BException
- */
private TLAType visitOpApplNode(OpApplNode n, TLAType expected) throws TLA2BException {
switch (n.getOperator().getKind()) {
@@ -497,19 +472,13 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
- /**
- * @param exprNode
- * @param expected
- * @return {@link TLAType}
- * @throws TLA2BException
- */
private TLAType evalBuiltInKind(OpApplNode n, TLAType expected) throws TLA2BException {
switch (getOpCode(n.getOperator().getName())) {
- /**********************************************************************
+ /*
* equality and disequality: =, #, /=
- **********************************************************************/
+ */
case OPCODE_eq: // =
case OPCODE_noteq: // /=, #
{
@@ -524,9 +493,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance();
}
- /**********************************************************************
+ /*
* Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
- **********************************************************************/
+ */
case OPCODE_neg: // Negation
case OPCODE_lnot: // Negation
case OPCODE_cl: // $ConjList
@@ -548,9 +517,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance();
}
- /**********************************************************************
+ /*
* Quantification: \A x \in S : P or \E x \in S : P
- **********************************************************************/
+ */
case OPCODE_be: // \E x \in S : P
case OPCODE_bf: // \A x \in S : P
{
@@ -565,9 +534,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance();
}
- /**********************************************************************
+ /*
* Set Operators
- **********************************************************************/
+ */
case OPCODE_se: // SetEnumeration {..}
{
SetType found = new SetType(new UntypedType());
@@ -626,9 +595,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance();
}
- /**********************************************************************
+ /*
* Set Constructor
- **********************************************************************/
+ */
case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
{
@@ -684,9 +653,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return setOfSet.getSubType();
}
- /**********************************************************************
+ /*
* Prime
- **********************************************************************/
+ */
case OPCODE_prime: // prime
{
try {
@@ -702,9 +671,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
}
- /***********************************************************************
+ /*
* Tuple: Tuple as Function 1..n to Set (Sequence)
- ***********************************************************************/
+ */
case OPCODE_tup: { // $Tuple
ArrayList<TLAType> list = new ArrayList<TLAType>();
for (int i = 0; i < n.getArgs().length; i++) {
@@ -733,9 +702,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /***********************************************************************
+ /*
* Function constructors
- ***********************************************************************/
+ */
case OPCODE_rfs: // recursive function ( f[x\in Nat] == IF x = 0 THEN 1
// ELSE f[n-1]
{
@@ -782,9 +751,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /***********************************************************************
+ /*
* Function call
- ***********************************************************************/
+ */
case OPCODE_fa: // $FcnApply f[1]
{
TLAType domType;
@@ -840,9 +809,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
- /***********************************************************************
+ /*
* Domain of Function
- ***********************************************************************/
+ */
case OPCODE_domain: {
FunctionType func = new FunctionType(new UntypedType(), new UntypedType());
@@ -856,9 +825,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
return res;
}
- /***********************************************************************
+ /*
* Set of Function
- ***********************************************************************/
+ */
case OPCODE_sof: // [ A -> B]
{
SetType A = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
@@ -874,17 +843,17 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /**********************************************************************
+ /*
* Except
- **********************************************************************/
+ */
case OPCODE_exc: // $Except
{
return evalExcept(n, expected);
}
- /***********************************************************************
+ /*
* Cartesian Product: A \X B
- ***********************************************************************/
+ */
case OPCODE_cp: // $CartesianProd A \X B \X C as $CartesianProd(A, B, C)
{
ArrayList<TLAType> list = new ArrayList<TLAType>();
@@ -903,9 +872,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /***********************************************************************
+ /*
* Records
- ***********************************************************************/
+ */
case OPCODE_sor: // $SetOfRcds [L1 : e1, L2 : e2]
{
StructType struct = new StructType();
@@ -969,9 +938,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return r.getType(fieldName);
}
- /***********************************************************************
+ /*
* miscellaneous constructs
- ***********************************************************************/
+ */
case OPCODE_ite: // IF THEN ELSE
{
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
@@ -985,12 +954,12 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
case OPCODE_case: {
- /**
+ /*
* CASE p1 -> e1 [] p2 -> e2 represented as $Case( $Pair(p1,
* e1),$Pair(p2, e2) ) and CASE p1 -> e1 [] p2 -> e2 [] OTHER -> e3
* represented as $Case( $Pair(p1, e1), $Pair(p2, e2), $Pair(null,
* e3))
- **/
+ */
TLAType found = expected;
for (int i = 0; i < n.getArgs().length; i++) {
OpApplNode pair = (OpApplNode) n.getArgs()[i];
@@ -1046,9 +1015,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance().unify(expected);
}
- /***********************************************************************
+ /*
* no TLA+ Built-ins
- ***********************************************************************/
+ */
case 0: {
return evalBBuiltIns(n, expected);
}
@@ -1126,12 +1095,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return domType;
}
- /**
- * @param n
- * @param expected
- * @return
- * @throws TLA2BException
- */
private TLAType evalExcept(OpApplNode n, TLAType expected) throws TLA2BException {
TLAType t = visitExprOrOpArgNode(n.getArgs()[0], expected);
n.setToolObject(TYPE_ID, t);
@@ -1199,12 +1162,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
- /**
- * @param list
- * @param valueType
- * @return
- * @throws TLA2BException
- */
private TLAType evalType(LinkedList<ExprOrOpArgNode> list, TLAType valueType) throws TLA2BException {
if (list.size() == 0) {
return valueType;
@@ -1225,9 +1182,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
switch (BBuiltInOPs.getOpcode(n.getOperator().getName())) {
// B Builtins
- /**********************************************************************
+ /*
* Standard Module Naturals
- **********************************************************************/
+ */
case B_OPCODE_gt: // >
case B_OPCODE_lt: // <
case B_OPCODE_leq: // <=
@@ -1290,9 +1247,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
}
- /**********************************************************************
+ /*
* Standard Module Integers
- **********************************************************************/
+ */
case B_OPCODE_int: // Int
{
try {
@@ -1317,9 +1274,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return IntType.getInstance();
}
- /**********************************************************************
+ /*
* Standard Module FiniteSets
- **********************************************************************/
+ */
case B_OPCODE_finite: // IsFiniteSet
{
try {
@@ -1344,9 +1301,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return IntType.getInstance();
}
- /**********************************************************************
+ /*
* Standard Module Sequences
- **********************************************************************/
+ */
case B_OPCODE_seq: { // Seq(S) - set of sequences, S must be a set
SetType S = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
@@ -1441,9 +1398,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
// TODO add BSeq to tla standard modules
- /**********************************************************************
+ /*
* Standard Module TLA2B
- **********************************************************************/
+ */
case B_OPCODE_min: // MinOfSet(S)
case B_OPCODE_max: // MaxOfSet(S)
@@ -1472,9 +1429,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /**********************************************************************
+ /*
* Standard Module TLA2B
- **********************************************************************/
+ */
case B_OPCODE_pow1: // POW1
{
@@ -1490,9 +1447,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /**********************************************************************
+ /*
* Standard Module Relations
- **********************************************************************/
+ */
case B_OPCODE_rel_inverse: // POW1
{
SetType set = new SetType(new TupleType(2));
@@ -1511,9 +1468,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /***********************************************************************
+ /*
* TLA+ Built-Ins, but not in tlc.tool.BuiltInOPs
- ***********************************************************************/
+ */
case B_OPCODE_bool: // BOOLEAN
try {
SetType found = new SetType(BoolType.getInstance());
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index 9c2c6f5..7070760 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.config;
import java.util.ArrayList;
@@ -75,11 +71,6 @@ public class ConfigfileEvaluator {
// configuration file. All constants with arguments have to be overridden in
// the configuration file.
-
- /**
- * @param configAst
- * @param moduleNode
- */
public ConfigfileEvaluator(ModelConfig configAst, ModuleNode moduleNode) {
this.configAst = configAst;
this.moduleNode = moduleNode;
@@ -116,10 +107,6 @@ public class ConfigfileEvaluator {
this.enumeratedTypes = new LinkedHashMap<String, EnumType>();
}
- /**
- * @throws ConfigFileErrorException
- *
- */
public void start() throws ConfigFileErrorException {
evalNext(); // check if NEXT declaration is a valid definition
evalInit(); // check if INIT declaration is a valid definition
@@ -214,9 +201,7 @@ public class ConfigfileEvaluator {
}
/**
- * Represents a override statement in the configuration file: k <- def
- *
- * @throws ConfigFileErrorException
+ * Represents a override statement in the configuration file: k <- def
*/
@SuppressWarnings("unchecked")
private void evalConstantOrDefOverrides() throws ConfigFileErrorException {
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index 40b92b2..1b6108c 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.config;
import java.util.Hashtable;
@@ -26,10 +22,6 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
private Hashtable<OpDefNode, OpDefNode> operatorOverrideTable;
private Hashtable<OpDefNode, ValueObj> operatorAssignments;
- /**
- * @param constantOverrideTable
- * @param operatorOverrideTable
- */
public ModuleOverrider(ModuleNode moduleNode,
Hashtable<OpDeclNode, OpDefNode> constantOverrideTable,
Hashtable<OpDefNode, OpDefNode> operatorOverrideTable,
@@ -40,10 +32,6 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
this.operatorAssignments = operatorAssignments;
}
- /**
- * @param moduleNode
- * @param conEval
- */
public ModuleOverrider(ModuleNode moduleNode, ConfigfileEvaluator conEval) {
this.moduleNode = moduleNode;
this.constantOverrideTable = conEval.getConstantOverrideTable();
@@ -109,9 +97,6 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
}
}
- /**
- * @param body
- */
private OpApplNode visitExprNode(ExprNode n) {
switch (n.getKind()) {
@@ -140,9 +125,6 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
return null;
}
- /**
- * @param n
- */
private OpApplNode visitOpApplNode(OpApplNode n) {
SymbolNode s = n.getOperator();
switch (s.getKind()) {
diff --git a/src/main/java/de/tla2b/config/TLCValueNode.java b/src/main/java/de/tla2b/config/TLCValueNode.java
index f8d9d0e..5878606 100644
--- a/src/main/java/de/tla2b/config/TLCValueNode.java
+++ b/src/main/java/de/tla2b/config/TLCValueNode.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.config;
import de.tla2b.global.TranslationGlobals;
@@ -16,11 +12,6 @@ public class TLCValueNode extends NumeralNode implements TranslationGlobals {
private Value value;
private TLAType type;
- /**
- * @param valObj
- * @param stn
- * @throws AbortException
- */
public TLCValueNode(ValueObj valObj, TreeNode stn) throws AbortException {
super("1337", stn);
this.value = valObj.getValue();
diff --git a/src/main/java/de/tla2b/config/ValueObj.java b/src/main/java/de/tla2b/config/ValueObj.java
index 668add5..85b95f9 100644
--- a/src/main/java/de/tla2b/config/ValueObj.java
+++ b/src/main/java/de/tla2b/config/ValueObj.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.config;
import de.tla2b.types.TLAType;
diff --git a/src/main/java/de/tla2b/exceptions/SemanticErrorException.java b/src/main/java/de/tla2b/exceptions/SemanticErrorException.java
index 6af42f0..7708c8b 100644
--- a/src/main/java/de/tla2b/exceptions/SemanticErrorException.java
+++ b/src/main/java/de/tla2b/exceptions/SemanticErrorException.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.exceptions;
@SuppressWarnings("serial")
diff --git a/src/main/java/de/tla2b/exceptions/UnificationException.java b/src/main/java/de/tla2b/exceptions/UnificationException.java
index 710fbc9..8ca36d7 100644
--- a/src/main/java/de/tla2b/exceptions/UnificationException.java
+++ b/src/main/java/de/tla2b/exceptions/UnificationException.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.exceptions;
@SuppressWarnings("serial")
public class UnificationException extends TLA2BException{
diff --git a/src/main/java/de/tla2b/global/TranslationGlobals.java b/src/main/java/de/tla2b/global/TranslationGlobals.java
index 938cfc3..cc159df 100644
--- a/src/main/java/de/tla2b/global/TranslationGlobals.java
+++ b/src/main/java/de/tla2b/global/TranslationGlobals.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.global;
import java.util.ArrayList;
diff --git a/src/main/java/de/tla2b/types/EnumType.java b/src/main/java/de/tla2b/types/EnumType.java
index c0ce831..a78c0fe 100644
--- a/src/main/java/de/tla2b/types/EnumType.java
+++ b/src/main/java/de/tla2b/types/EnumType.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.types;
import java.util.ArrayList;
@@ -12,8 +8,6 @@ import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
import de.tla2bAst.BAstCreator;
-
-
public class EnumType extends AbstractHasFollowers {
public LinkedHashSet<String> modelvalues;
public int id;
@@ -90,4 +84,4 @@ public class EnumType extends AbstractHasFollowers {
}
-}
\ No newline at end of file
+}
diff --git a/src/main/java/de/tla2b/types/StringType.java b/src/main/java/de/tla2b/types/StringType.java
index 13b5623..8e507fd 100644
--- a/src/main/java/de/tla2b/types/StringType.java
+++ b/src/main/java/de/tla2b/types/StringType.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.types;
import de.be4.classicalb.core.parser.node.AStringSetExpression;
diff --git a/src/main/java/de/tla2b/types/StructOrFunctionType.java b/src/main/java/de/tla2b/types/StructOrFunctionType.java
index fc4aea1..0243e92 100644
--- a/src/main/java/de/tla2b/types/StructOrFunctionType.java
+++ b/src/main/java/de/tla2b/types/StructOrFunctionType.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.types;
import java.util.Iterator;
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 46c2d55..df56ca7 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -87,9 +87,6 @@ public class BAstCreator extends BuiltInOPs
/**
* Creates a B AST node for a TLA expression
- *
- * @param moduleNode
- * @param specAnalyser
*/
public BAstCreator(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
@@ -996,9 +993,9 @@ public class BAstCreator extends BuiltInOPs
returnNode = new ABooleanFalseExpression();
break;
- /**********************************************************************
+ /*
* Standard Module Naturals
- **********************************************************************/
+ */
case B_OPCODE_nat: // Nat
returnNode = new ANaturalSetExpression();
break;
@@ -1098,9 +1095,9 @@ public class BAstCreator extends BuiltInOPs
case B_OPCODE_string: // STRING
returnNode = new AStringSetExpression();
break;
- /**********************************************************************
+ /*
* Standard Module Sequences
- **********************************************************************/
+ */
case B_OPCODE_seq: // Seq(S) - set of sequences
returnNode = new ASeqExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
@@ -1295,9 +1292,9 @@ public class BAstCreator extends BuiltInOPs
return new AConvertBoolExpression(notEqual);
}
- /**********************************************************************
+ /*
* Set Operators
- **********************************************************************/
+ */
case OPCODE_se: // SetEnumeration {..}
{
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index ea33cfb..7fd7ee8 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -185,10 +185,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
return n;
}
- /**
- * @param moduleFileName
- * @throws de.tla2b.exceptions.FrontEndException
- */
private SpecObj parseModuleWithoutSemanticAnalyse(String moduleFileName,
String module) {
SpecObj spec = new SpecObj(moduleFileName, null);
@@ -211,10 +207,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
return spec;
}
- /**
- * @param spec
- * @return
- */
private void evalVariables(SpecObj spec, String moduleName) {
ParseUnit p = (ParseUnit) spec.parseUnitContext.get(moduleName);
TreeNode n_module = p.getParseTree();
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 7395892..ad5ce0c 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -94,12 +94,6 @@ public class Translator implements TranslationGlobals {
/**
* External interface
- *
- * @param moduleName
- * @param moduleString
- * @param configString
- * @return
- * @throws TLA2BException
*/
public static String translateModuleString(String moduleName, String moduleString, String configString)
throws TLA2BException {
diff --git a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
index c1722d8..69bfaa6 100644
--- a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.expression;
import org.junit.Test;
diff --git a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
index 97e570c..01f1577 100644
--- a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.expression;
import org.junit.Test;
diff --git a/src/test/java/de/tla2b/expression/TestError.java b/src/test/java/de/tla2b/expression/TestError.java
index 104ff1b..63f113b 100644
--- a/src/test/java/de/tla2b/expression/TestError.java
+++ b/src/test/java/de/tla2b/expression/TestError.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.expression;
import static de.tla2b.util.TestUtil.compareExpr;
diff --git a/src/test/java/de/tla2b/expression/TestKeywords.java b/src/test/java/de/tla2b/expression/TestKeywords.java
index ef4ecec..7516dae 100644
--- a/src/test/java/de/tla2b/expression/TestKeywords.java
+++ b/src/test/java/de/tla2b/expression/TestKeywords.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.expression;
import org.junit.Test;
diff --git a/src/test/java/de/tla2b/expression/TestSequences.java b/src/test/java/de/tla2b/expression/TestSequences.java
index 9fabeec..123e10a 100644
--- a/src/test/java/de/tla2b/expression/TestSequences.java
+++ b/src/test/java/de/tla2b/expression/TestSequences.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.expression;
import static de.tla2b.util.TestUtil.compareExpr;
diff --git a/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java b/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
index 6570544..98b5c65 100644
--- a/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
diff --git a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
index e2a58e5..351f4f1 100644
--- a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
@@ -98,9 +94,9 @@ public class FunctionTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* recursive Function
- **********************************************************************/
+ */
@Ignore
@Test
@@ -122,9 +118,9 @@ public class FunctionTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Function call
- **********************************************************************/
+ */
@Test
public void testFunctionCall() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
index 5293734..6cf231b 100644
--- a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import org.junit.Test;
@@ -43,9 +39,9 @@ public class LogicOperatorsTest {
compare(expected, module);
}
- /**********************************************************************
- * Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
- **********************************************************************/
+ /*
+ * Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
+ */
@Test
public void testAnd() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -71,9 +67,9 @@ public class LogicOperatorsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Negation: ~, \neg, \lnot
- **********************************************************************/
+ */
@Test
public void testNegation() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -84,9 +80,9 @@ public class LogicOperatorsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Implication and Equivalence: =>, \equiv
- **********************************************************************/
+ */
@Test
public void testImplication() throws Exception {
@@ -112,9 +108,9 @@ public class LogicOperatorsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Quantification: \A x \in S : P or \E x \in S : P
- **********************************************************************/
+ */
@Test
public void testUniversalQuantifier() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java b/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java
index fa457c9..bb851df 100644
--- a/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
diff --git a/src/test/java/de/tla2b/prettyprintb/RecordTest.java b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
index c956984..c837c85 100644
--- a/src/test/java/de/tla2b/prettyprintb/RecordTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
@@ -16,9 +12,9 @@ public class RecordTest {
ToolIO.setMode(ToolIO.TOOL);
}
- /**********************************************************************
+ /*
* Set of Records: [L1 : e1, L2 : e2]
- **********************************************************************/
+ */
@Test
public void testStruct() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -34,9 +30,9 @@ public class RecordTest {
}
- /**********************************************************************
+ /*
* Record: [L1 |-> e1, L2 |-> e2]
- **********************************************************************/
+ */
@Test
public void testRecord() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -65,9 +61,9 @@ public class RecordTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Record Select: r.c
- **********************************************************************/
+ */
@Test
public void testRecordSelect() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -94,9 +90,9 @@ public class RecordTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Record Except
- **********************************************************************/
+ */
@Test
public void testRecordExcept() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -110,9 +106,9 @@ public class RecordTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Record Except @
- **********************************************************************/
+ */
@Test
public void testRecordExceptAt() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/prettyprintb/SetsTest.java b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
index e9739e2..cbc5b00 100644
--- a/src/test/java/de/tla2b/prettyprintb/SetsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
@@ -34,9 +30,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Element of: \in, \notin
- **********************************************************************/
+ */
@Test
public void testMemberOf() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -68,9 +64,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* set operators like difference, union, intersection: \setdiff, \cup, \cap
- **********************************************************************/
+ */
@Test
public void testSetDifference() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -104,9 +100,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Subseteq: subset or equal
- **********************************************************************/
+ */
@Test
public void testSubsteq() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -118,9 +114,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* SUBSET: conforms POW in B
- **********************************************************************/
+ */
@Test
public void testSubset() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -132,9 +128,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* UNION
- **********************************************************************/
+ */
@Test
public void testUnion() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -146,9 +142,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Set Constructor
- **********************************************************************/
+ */
@Test
public void testConstructor1() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/prettyprintb/TupleTest.java b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
index 8001764..8528ef4 100644
--- a/src/test/java/de/tla2b/prettyprintb/TupleTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
diff --git a/src/test/java/de/tla2b/prettyprintb/VariablesTest.java b/src/test/java/de/tla2b/prettyprintb/VariablesTest.java
index 386aa91..1188100 100644
--- a/src/test/java/de/tla2b/prettyprintb/VariablesTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/VariablesTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
diff --git a/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java
index 7daa5a4..8c64d97 100644
--- a/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb.standardmodules;
import static de.tla2b.util.TestUtil.compare;
diff --git a/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java
index 47c88dc..58cc1c4 100644
--- a/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb.standardmodules;
import static de.tla2b.util.TestUtil.compare;
@@ -13,9 +9,9 @@ import org.junit.Test;
public class ModuleNaturalsTest {
- /**********************************************************************
+ /*
* >, <, <=, >=
- **********************************************************************/
+ */
@Test
public void testCompareOperators() throws Exception {
@@ -41,9 +37,9 @@ public class ModuleNaturalsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Arithmetic operator: +, -, *, %, ^ (\div operator is not tested)
- **********************************************************************/
+ */
@Test
public void testArithmeticOperators() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -56,9 +52,9 @@ public class ModuleNaturalsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Interval operator: x .. y
- **********************************************************************/
+ */
@Test
public void testDotDot() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
index a79f3b6..5a9954b 100644
--- a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
+++ b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.*;
@@ -18,9 +14,9 @@ import de.tla2b.util.TestUtil;
public class BBuiltInsTest {
- /**********************************************************************
+ /*
* BOOLEAN
- **********************************************************************/
+ */
@Test
public void testBoolean() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -42,9 +38,9 @@ public class BBuiltInsTest {
}
- /**********************************************************************
+ /*
* String
- **********************************************************************/
+ */
@Test
public void testString() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -64,9 +60,9 @@ public class BBuiltInsTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Bool value: TRUE, FALSE
- **********************************************************************/
+ */
@Test
public void testBoolValue() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/ConfigTest.java b/src/test/java/de/tla2b/typechecking/ConfigTest.java
index ff938d0..2968bce 100644
--- a/src/test/java/de/tla2b/typechecking/ConfigTest.java
+++ b/src/test/java/de/tla2b/typechecking/ConfigTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java b/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
index f3c7471..998607a 100644
--- a/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
+++ b/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.*;
diff --git a/src/test/java/de/tla2b/typechecking/DefinitionsTest.java b/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
index 954fe82..e1a65ae 100644
--- a/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
+++ b/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.*;
@@ -16,9 +12,9 @@ import de.tla2b.util.TestUtil;
public class DefinitionsTest {
- /**********************************************************************
+ /*
* Definition: foo(a,b) == e
- **********************************************************************/
+ */
@Test
public void testDefinition() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -72,9 +68,9 @@ public class DefinitionsTest {
assertEquals("BOOL", t.getConstantType("k2"));
}
- /**********************************************************************
+ /*
* Definition Call
- **********************************************************************/
+ */
@Test
public void testDefinitionCall() throws FrontEndException, TLA2BException {
diff --git a/src/test/java/de/tla2b/typechecking/ExceptTest.java b/src/test/java/de/tla2b/typechecking/ExceptTest.java
index 82d4cc1..5531720 100644
--- a/src/test/java/de/tla2b/typechecking/ExceptTest.java
+++ b/src/test/java/de/tla2b/typechecking/ExceptTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/ExtendsTest.java b/src/test/java/de/tla2b/typechecking/ExtendsTest.java
index 95e7ced..a62dca2 100644
--- a/src/test/java/de/tla2b/typechecking/ExtendsTest.java
+++ b/src/test/java/de/tla2b/typechecking/ExtendsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/FunctionTest.java b/src/test/java/de/tla2b/typechecking/FunctionTest.java
index a73ea0b..e12fda6 100644
--- a/src/test/java/de/tla2b/typechecking/FunctionTest.java
+++ b/src/test/java/de/tla2b/typechecking/FunctionTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class FunctionTest {
- /**********************************************************************
+ /*
* Function constructor
- **********************************************************************/
+ */
@Test
public void testSimpleFunctionConstructor() throws FrontEndException,
@@ -165,9 +161,9 @@ public class FunctionTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* recursive Function
- **********************************************************************/
+ */
@Test
public void testRecursiveFunction() throws FrontEndException,
TLA2BException {
@@ -183,9 +179,9 @@ public class FunctionTest {
assertEquals("INTEGER", t.getConstantType("k3"));
}
- /**********************************************************************
+ /*
* Function call
- **********************************************************************/
+ */
@Test
public void testFunctionCall() throws FrontEndException, TLA2BException {
@@ -244,9 +240,9 @@ public class FunctionTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Domain
- **********************************************************************/
+ */
@Test
public void testDomain() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -273,9 +269,9 @@ public class FunctionTest {
assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k2"));
}
- /**********************************************************************
+ /*
* Set of Function
- **********************************************************************/
+ */
@Test
public void testSetOfFunction() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -310,9 +306,9 @@ public class FunctionTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Except
- **********************************************************************/
+ */
@Test
public void testFunctionExcept() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -412,9 +408,9 @@ public class FunctionTest {
assertEquals("POW(INTEGER*INTEGER*INTEGER)", t.getConstantType("k"));
}
- /**********************************************************************
+ /*
* Except @
- **********************************************************************/
+ */
@Test
public void testAt2() throws FrontEndException, TLA2BException {
diff --git a/src/test/java/de/tla2b/typechecking/InstanceTest.java b/src/test/java/de/tla2b/typechecking/InstanceTest.java
index 329a772..6ac9c7d 100644
--- a/src/test/java/de/tla2b/typechecking/InstanceTest.java
+++ b/src/test/java/de/tla2b/typechecking/InstanceTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
index f4585bf..c46e2f7 100644
--- a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.*;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class LogicOperatorsTest {
- /**********************************************************************
+ /*
* equality and disequality: =, #,
- **********************************************************************/
+ */
@Test
public void testEquality() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -48,9 +44,9 @@ public class LogicOperatorsTest {
- /**********************************************************************
+ /*
* Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
- **********************************************************************/
+ */
@Test
public void testLogicOperators() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -73,9 +69,9 @@ public class LogicOperatorsTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Quantification: \A x \in S : P or \E x \in S : P.
- **********************************************************************/
+ */
@Test
diff --git a/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java b/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
index e49d769..6ed199b 100644
--- a/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
+++ b/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
@@ -16,9 +12,9 @@ import de.tla2b.util.TestUtil;
public class MiscellaneousConstructsTest {
- /**********************************************************************
+ /*
* IF THEN ELSE
- **********************************************************************/
+ */
@Test
public void testIfThenElse() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -33,9 +29,9 @@ public class MiscellaneousConstructsTest {
}
- /**********************************************************************
+ /*
* IF THEN ELSE
- **********************************************************************/
+ */
@Test
public void testCase() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -65,9 +61,9 @@ public class MiscellaneousConstructsTest {
assertEquals("INTEGER",t.getConstantType("e3"));
}
- /**********************************************************************
+ /*
* LET d == exp IN e
- **********************************************************************/
+ */
@Test
public void testLetIn() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/OpArgTest.java b/src/test/java/de/tla2b/typechecking/OpArgTest.java
index a000e9b..0c96a26 100644
--- a/src/test/java/de/tla2b/typechecking/OpArgTest.java
+++ b/src/test/java/de/tla2b/typechecking/OpArgTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/SetTest.java b/src/test/java/de/tla2b/typechecking/SetTest.java
index 4fad92a..3d5c323 100644
--- a/src/test/java/de/tla2b/typechecking/SetTest.java
+++ b/src/test/java/de/tla2b/typechecking/SetTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.*;
@@ -14,15 +10,11 @@ import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
-import tla2sany.semantic.AbortException;
-
public class SetTest {
- /**********************************************************************
+ /*
* Set Enumeration: {1,2,3}
- *
- * @throws AbortException
- **********************************************************************/
+ */
@Test
public void testSetEnumeration() throws FrontEndException, TLA2BException {
@@ -97,9 +89,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Element of: \in, \notin
- **********************************************************************/
+ */
@Test
public void testElementOfSet() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -150,9 +142,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* set operators like difference, union, intersection
- **********************************************************************/
+ */
@Test
public void testSetOperators() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -196,9 +188,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* set constructor: {x \in S : p}.
- **********************************************************************/
+ */
@Test
public void testSubsetOf() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -310,9 +302,9 @@ public class SetTest {
assertEquals("POW(INTEGER*BOOL)", t.getConstantType("S"));
}
- /**********************************************************************
+ /*
* set constructor: {e : x \in S}
- **********************************************************************/
+ */
@Test
public void testSetOfAll() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -391,9 +383,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* SUBSET: conforms POW in B
- **********************************************************************/
+ */
@Test
public void testSubset() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -425,9 +417,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* UNION
- **********************************************************************/
+ */
@Test
public void testUnion() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -468,9 +460,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Subseteq: subset or equal
- **********************************************************************/
+ */
@Test
public void testSubseteq() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/StringTest.java b/src/test/java/de/tla2b/typechecking/StringTest.java
index 4ae59ce..e606c6b 100644
--- a/src/test/java/de/tla2b/typechecking/StringTest.java
+++ b/src/test/java/de/tla2b/typechecking/StringTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class StringTest {
- /**********************************************************************
+ /*
* a String: "abc"
- **********************************************************************/
+ */
@Test
public void testAString() throws FrontEndException, TLA2BException {
@@ -67,9 +63,9 @@ public class StringTest {
}
- /**********************************************************************
+ /*
* STRING
- **********************************************************************/
+ */
@Test
public void testString() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/StructTest.java b/src/test/java/de/tla2b/typechecking/StructTest.java
index e9ef276..3b577f5 100644
--- a/src/test/java/de/tla2b/typechecking/StructTest.java
+++ b/src/test/java/de/tla2b/typechecking/StructTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
@@ -20,9 +16,9 @@ public class StructTest {
ToolIO.setMode(ToolIO.TOOL);
}
- /**********************************************************************
+ /*
* Set of Records: [L1 : e1, L2 : e2]
- **********************************************************************/
+ */
@Test
public void testStruct() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -84,9 +80,9 @@ public class StructTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Record: [L1 |-> e1, L2 |-> e2]
- **********************************************************************/
+ */
@Test
public void testRecord() throws FrontEndException, TLA2BException {
@@ -128,9 +124,9 @@ public class StructTest {
assertEquals("BOOL", t.getConstantType("k2"));
}
- /**********************************************************************
+ /*
* Record Select: r.c
- **********************************************************************/
+ */
@Test
public void testRecordSelect() throws FrontEndException, TLA2BException {
@@ -220,9 +216,9 @@ public class StructTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Record Except
- **********************************************************************/
+ */
@Test
public void testRecordExcept() throws FrontEndException, TLA2BException {
@@ -248,9 +244,9 @@ public class StructTest {
assertEquals("struct(a:INTEGER,b:BOOL)", t.getConstantType("k2"));
}
- /**********************************************************************
+ /*
* Record Except @
- **********************************************************************/
+ */
@Test
public void testRecordExceptAt() throws FrontEndException, TLA2BException {
diff --git a/src/test/java/de/tla2b/typechecking/TupleTest.java b/src/test/java/de/tla2b/typechecking/TupleTest.java
index 48b0fb9..2581f92 100644
--- a/src/test/java/de/tla2b/typechecking/TupleTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleTest.java
@@ -157,9 +157,9 @@ public class TupleTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Cartesian Product
- **********************************************************************/
+ */
@Test
public void testCartesianProduct2() throws FrontEndException,
TLA2BException {
diff --git a/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java b/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
index 413014f..9dd382d 100644
--- a/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
+++ b/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import org.junit.Test;
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
index fa93e1d..44c102b 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking.standardmodules;
import static org.junit.Assert.*;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class TestModuleFiniteSets {
- /**********************************************************************
+ /*
* IsFiniteSet
- **********************************************************************/
+ */
@Test
public void unifyIsFiniteSet() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -73,9 +69,9 @@ public class TestModuleFiniteSets {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Cardinality
- **********************************************************************/
+ */
@Test
public void unifyCardinality() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
index b658435..66941f4 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking.standardmodules;
import static org.junit.Assert.*;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class TestModuleIntegers {
- /**********************************************************************
+ /*
* Int
- **********************************************************************/
+ */
@Test
public void unifyInt() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -40,9 +36,9 @@ public class TestModuleIntegers {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* unary minus: -x
- **********************************************************************/
+ */
@Test
public void unifyUnaryMinus() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
index 3fa055d..5d6501c 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking.standardmodules;
import static org.junit.Assert.assertEquals;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class TestModuleNaturals {
- /**********************************************************************
+ /*
* Relational operators: >, <, <=, >=
- **********************************************************************/
+ */
@Test
public void testRelationalOperators() throws FrontEndException,
TLA2BException {
@@ -44,9 +40,9 @@ public class TestModuleNaturals {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Arithmetic operator: +, -, *, /, mod, exp
- **********************************************************************/
+ */
@Test
public void testArithmeticOperators() throws FrontEndException,
TLA2BException {
@@ -72,9 +68,9 @@ public class TestModuleNaturals {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Interval operator: x .. y
- **********************************************************************/
+ */
@Test
public void testDotDot() throws FrontEndException, TLA2BException {
@@ -99,9 +95,9 @@ public class TestModuleNaturals {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Nat
- **********************************************************************/
+ */
@Test
public void testNat() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
index 0ae160f..7eccb44 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking.standardmodules;
import static org.junit.Assert.*;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class TestModuleSequences {
- /**********************************************************************
+ /*
* Seq(S): The set of all sequences of elements in S.
- **********************************************************************/
+ */
@Test
public void testSeq() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -64,9 +60,9 @@ public class TestModuleSequences {
}
- /**********************************************************************
+ /*
* Len(S)
- **********************************************************************/
+ */
@Test
public void testLen() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -109,9 +105,9 @@ public class TestModuleSequences {
}
- /**********************************************************************
+ /*
* s \o s2 - concatenation of s and s2
- **********************************************************************/
+ */
@Test
public void testUnifyConcatenation() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -180,9 +176,9 @@ public class TestModuleSequences {
}
- /**********************************************************************
+ /*
* Append(s, e)
- **********************************************************************/
+ */
@Test
public void testUnifyAppend() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -237,9 +233,9 @@ public class TestModuleSequences {
}
- /**********************************************************************
+ /*
* Head(s): the first element of the seq
- **********************************************************************/
+ */
@Test
public void testUnifyHead() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -274,9 +270,9 @@ public class TestModuleSequences {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Tail(s): the sequence without the first element
- **********************************************************************/
+ */
@Test
public void testUnifyTail() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -312,9 +308,9 @@ public class TestModuleSequences {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* SubSeq(s,m,n): The sequence <<s[m], s[m+1], ... , s[n]>>
- **********************************************************************/
+ */
@Test
public void testUnifySubSeq() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index 2dd2c11..5e7af8b 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.util;
import java.util.Hashtable;
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 0781ae2..d0d9cf7 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.util;
import static org.junit.Assert.*;
--
GitLab