From 4b8203fe11a425633d86bffd8d5ad1fba2877627 Mon Sep 17 00:00:00 2001 From: Edward Sabinus <edward.sabinus@informatik.uni-halle.de> Date: Fri, 15 Dec 2023 13:59:59 +0100 Subject: [PATCH] repaired name of AbstractEingabeverwalter, changed all possible errors to nondeadly in Listener_Helper and ADT_Listener, Added Tests for ADT for non deadly semantic errors --- ...rwalter.cs => AbstractEingabeverwalter.cs} | 4 +- .../Eingabeverwaltung/Eingabeverwalter.cs | 5 +- .../Eingabeverwaltung/Parser/ADT_Antlr.cs | 6 +- .../Eingabeverwaltung/Parser/ADT_Listener.cs | 36 +++++------ .../Parser/Listener_Helper.cs | 41 ++++++++++--- .../SimpleEingabeverwalter.cs | 2 +- .../Eingabeverwaltung/TestEingabeverwalter.cs | 60 +++++++++++++++++++ .../Testverwaltung/ExtraTest.cs | 45 +++++++++++++- .../Testverwaltung/Test.cs | 4 +- .../Tests/extra/NonDeadSemErrs/0riginal.adt | 11 ++++ .../Tests/extra/NonDeadSemErrs/ax.adt | 11 ++++ .../Tests/extra/NonDeadSemErrs/chaos.adt | 19 ++++++ .../Tests/extra/NonDeadSemErrs/op.adt | 12 ++++ .../Tests/extra/NonDeadSemErrs/sort.adt | 13 ++++ .../Tests/extra/NonDeadSemErrs/tree1.adt | 12 ++++ .../Tests/extra/NonDeadSemErrs/tree2.adt | 12 ++++ .../Tests/extra/NonDeadSemErrs/tree3.adt | 12 ++++ .../Tests/extra/NonDeadSemErrs/tree4.adt | 12 ++++ .../Tests/extra/NonDeadSemErrs/tree5.adt | 12 ++++ 19 files changed, 292 insertions(+), 37 deletions(-) rename BewerterStrukturellerInduktion/Eingabeverwaltung/{AbstactEingabeverwalter.cs => AbstractEingabeverwalter.cs} (75%) create mode 100644 BewerterStrukturellerInduktion/Eingabeverwaltung/TestEingabeverwalter.cs create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.adt create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/ax.adt create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/chaos.adt create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/op.adt create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/sort.adt create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree1.adt create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree2.adt create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree3.adt create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree4.adt create mode 100644 BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree5.adt diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/AbstactEingabeverwalter.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/AbstractEingabeverwalter.cs similarity index 75% rename from BewerterStrukturellerInduktion/Eingabeverwaltung/AbstactEingabeverwalter.cs rename to BewerterStrukturellerInduktion/Eingabeverwaltung/AbstractEingabeverwalter.cs index 229fac9..958b626 100644 --- a/BewerterStrukturellerInduktion/Eingabeverwaltung/AbstactEingabeverwalter.cs +++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/AbstractEingabeverwalter.cs @@ -3,11 +3,11 @@ namespace Eingabeverwaltung { - public abstract class AbstactEingabeverwalter + public abstract class AbstractEingabeverwalter { protected Container inputContainer; - public AbstactEingabeverwalter() + public AbstractEingabeverwalter() { inputContainer = null; } diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Eingabeverwalter.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Eingabeverwalter.cs index 8e9fdc0..c320c3a 100644 --- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Eingabeverwalter.cs +++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Eingabeverwalter.cs @@ -7,7 +7,7 @@ using System.Collections.Generic; namespace Eingabeverwaltung { - public class Eingabeverwalter : AbstactEingabeverwalter + public class Eingabeverwalter : AbstractEingabeverwalter { public Eingabeverwalter() : base() { } @@ -135,7 +135,8 @@ namespace Eingabeverwaltung Console.WriteLine(a.Message); verwalteEingabe(); } - } + } + public void Eingabe_Interface(string action, string path) { ImmutableDictionary<string, Action<string>> eingabe = new Dictionary<string, Action<string>> diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Antlr.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Antlr.cs index ff28e49..9e20fcc 100644 --- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Antlr.cs +++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Antlr.cs @@ -19,10 +19,12 @@ namespace Eingabeverwaltung.Parser parser.BuildParseTree = true; ADTParser.AdtContext tree = parser.adt(); - IADTListener adt_Listener = new ADT_Listener(container); + Listener_Helper LH = new Listener_Helper(); + IADTListener adt_Listener = new ADT_Listener(container,LH); ParseTreeWalker.Default.Walk(adt_Listener, tree); + LH.close(); - return container.ADT; + return container.ADT; } } } diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Listener.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Listener.cs index 18cf9d1..3255407 100644 --- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Listener.cs +++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/ADT_Listener.cs @@ -19,23 +19,23 @@ namespace Eingabeverwaltung.Parser private Listener_Helper LH; - public ADT_Listener(Container container) + public ADT_Listener(Container container, Listener_Helper LH) { this.container = container; op_sorts = null; - LH = new Listener_Helper(null, null, null, null, null, null); + this.LH = LH; } public void EnterAdt([NotNull] ADTParser.AdtContext context) { } public void ExitAdt([NotNull] ADTParser.AdtContext context) { Coords coords = new Coords(context); - if (LH.adt_sorts == null) throw new KontextException(coords,"adt_sorts = null at ExitAdt"); - if (LH.adt_ops == null) throw new KontextException(coords,"adt_ops = null at ExitAdt"); + if (LH.adt_sorts == null) LH.errors.Add(new SemanticAnalysisError(coords,"adt_sorts = null at ExitAdt")); + if (LH.adt_ops == null) LH.errors.Add(new SemanticAnalysisError(coords,"adt_ops = null at ExitAdt")); if (LH.adt_axioms == null) LH.adt_axioms = new List<Axiom>(); - if (LH.adt_sorts.Count < 1) throw new KontextException(coords,"adt_sorts is empty at ExitAdt"); - if (LH.adt_ops.Count < 1) throw new KontextException(coords,"adt_ops is empty at ExitAdt"); + if (LH.adt_sorts.Count < 1) LH.errors.Add(new SemanticAnalysisError(coords, "adt_sorts is empty at ExitAdt")); + if (LH.adt_ops.Count < 1) LH.errors.Add(new SemanticAnalysisError(coords, "adt_ops is empty at ExitAdt")); container.ADT = new ADT(LH.adt_sorts, LH.adt_ops, LH.adt_axioms); } public void EnterName([NotNull] ADTParser.NameContext context) { } @@ -44,7 +44,7 @@ namespace Eingabeverwaltung.Parser public void EnterSorts([NotNull] ADTParser.SortsContext context) => LH.adt_sorts = new List<Sort>(); public void ExitSorts([NotNull] ADTParser.SortsContext context) { - if (LH.adt_sorts.Count < 1) throw new KontextException(new Coords(context),"adt_sorts is empty at ExitSorts"); + if (LH.adt_sorts.Count < 1) LH.errors.Add(new SemanticAnalysisError(new Coords(context),"adt_sorts is empty at ExitSorts")); } public void EnterSort([NotNull] ADTParser.SortContext context) { } @@ -66,17 +66,17 @@ namespace Eingabeverwaltung.Parser return; } if (context.Parent.Parent.GetChild(0).GetText() == "vars") return; // this job is done in ExitVar - throw new KontextException(coords,"ExitSort with Context = " + context.GetText() + " in parent "+ context.Parent.GetChild(0).GetText() + " was not able to find the sense of its life."); + throw new SemanticAnalysisDeadlyError(coords,"ExitSort with Context = " + context.GetText() + " in parent "+ context.Parent.GetChild(0).GetText() + " was not able to find the sense of its life."); } public void EnterConstructors([NotNull] ADTParser.ConstructorsContext context) => LH.adt_ops = new List<Operation>(); public void ExitConstructors([NotNull] ADTParser.ConstructorsContext context) { Coords coords = new Coords(context); - if (LH.adt_ops.Count < 1) throw new KontextException(coords,"adt_ops is empty at ExitConstructors"); + if (LH.adt_ops.Count < 1) LH.errors.Add(new SemanticAnalysisError(coords, "adt_ops is empty at ExitConstructors")); // check for each sort: numer & type of constructors is ok foreach (Sort sort in LH.adt_sorts) if (sort.GetBuildingConstructors().Count > 0 && sort.GetBasicConstructors().Count == 0) - throw new KontextException(coords,"The sort "+sort.name+" has building constructors, but no basic constructors."); + LH.errors.Add(new SemanticAnalysisError(coords,"The sort "+sort.name+" has building constructors, but no basic constructors.")); } public void EnterOperations([NotNull] ADTParser.OperationsContext context) @@ -85,14 +85,14 @@ namespace Eingabeverwaltung.Parser } public void ExitOperations([NotNull] ADTParser.OperationsContext context) { - if (LH.adt_ops.Count < 1) throw new KontextException(new Coords(context),"adt_ops is empty at ExitOperations"); + if (LH.adt_ops.Count < 1) LH.errors.Add(new SemanticAnalysisError(new Coords(context), "adt_ops is empty at ExitOperations")); } public void EnterOperation(ADTParser.OperationContext context) => op_sorts = new List<Sort>(); public void ExitOperation(ADTParser.OperationContext context) { Coords coords = new Coords(context); - if (op_sorts.Count < 1) throw new KontextException(coords,"op_sorts is empty at ExitOperation"); + if (op_sorts.Count < 1) LH.errors.Add(new SemanticAnalysisError(coords, "op_sorts is empty at ExitOperation")); string operationName = context.BEZ().GetText(); Test_Operations_all_unique(operationName,new Coords(context)); Operation operation; @@ -107,7 +107,7 @@ namespace Eingabeverwaltung.Parser else operation = new BuildingConstructor(operationName, op_sorts); op_sorts.Last().SetConstructor((Constructor)operation); } - else throw new KontextException(coords,"ExitOperation with Context = " + context.GetText() + " in parent " + context.Parent.GetChild(0).GetText() + " was not able to find the sense of its life."); + else throw new SemanticAnalysisDeadlyError(coords,"ExitOperation with Context = " + context.GetText() + " in parent " + context.Parent.GetChild(0).GetText() + " was not able to find the sense of its life."); LH.adt_ops.Add(operation); } @@ -121,7 +121,7 @@ namespace Eingabeverwaltung.Parser public void EnterAxioms([NotNull] ADTParser.AxiomsContext context) => LH.adt_axioms = new List<Axiom>(); public void ExitAxioms([NotNull] ADTParser.AxiomsContext context) { - if (LH.adt_axioms.Count < 1) throw new KontextException(new Coords(context),"adt_axioms is empty at ExitAxioms"); + if (LH.adt_axioms.Count < 1) LH.errors.Add(new SemanticAnalysisError(new Coords(context),"adt_axioms is empty at ExitAxioms")); } public void EnterAxiom([NotNull] ADTParser.AxiomContext context) => LH.trees = new List<Tree>(); @@ -185,7 +185,7 @@ namespace Eingabeverwaltung.Parser /// <param name="sortName"></param> private void Test_Sorts_all_unique(string sortName, Coords coords) { - if (LH.findSortInADT_Sorts(sortName) != null) throw new KontextException(coords,"The Sort " + sortName + " was defined more than 1 times in Sorts of ADT!"); + if (LH.findSortInADT_Sorts(sortName) != null) LH.errors.Add(new SemanticAnalysisError(coords,"The Sort " + sortName + " was defined more than 1 times in Sorts of ADT!")); } /// <summary> /// This Test is activated always when a new Operation gets added to the operationList of the ADT, @@ -194,7 +194,7 @@ namespace Eingabeverwaltung.Parser /// <param name="operationName"></param> private void Test_Operations_all_unique(string operationName, Coords coords) { - if (LH.findOperationInADT_Ops(operationName,0,false,coords) != null) throw new KontextException(coords,"The Operation " + operationName + " was defined more than 1 times in Operations of ADT!"); + if (LH.findOperationInADT_Ops(operationName,0,false,coords) != null) LH.errors.Add(new SemanticAnalysisError(coords, "The Operation " + operationName + " was defined more than 1 times in Operations of ADT!")); } /// <summary> /// This Test is activated always when a new Sort gets added to the sortList of an Operation, @@ -203,7 +203,7 @@ namespace Eingabeverwaltung.Parser /// <param name="sortName"></param> private void Test_Operation_all_Sorts_were_defined_in_ADT(string sortName, Coords coords) { - if (LH.findSortInADT_Sorts(sortName) == null) throw new KontextException(coords,"Found a Sort " + sortName + " in Operations that was not defined in Sorts!"); + if (LH.findSortInADT_Sorts(sortName) == null) LH.errors.Add(new SemanticAnalysisError(coords, "Found a Sort " + sortName + " in Operations that was not defined in Sorts!")); } /// <summary> /// This Test is activated always when a new Axiom gets added to the axiomList of the ADT, @@ -214,7 +214,7 @@ namespace Eingabeverwaltung.Parser { foreach (Axiom axiom in LH.adt_axioms) { - if (axiom.name == axiomName) throw new KontextException(coords,"The Axiom " + axiomName + " was defined more than 1 times in Axioms of ADT!"); + if (axiom.name == axiomName) LH.errors.Add(new SemanticAnalysisError(coords, "The Axiom " + axiomName + " was defined more than 1 times in Axioms of ADT!")); } } /// <summary> diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs index 5f75a56..b14ef12 100644 --- a/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs +++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/Parser/Listener_Helper.cs @@ -25,6 +25,8 @@ namespace Eingabeverwaltung.Parser public List<SemanticAnalysisError> errors; public List<SemanticAnalysisWarning> warnings; + public Listener_Helper() : this(null,null,null,null,null,null) { } + public Listener_Helper(List<Sort> adt_sorts, List<Operation> adt_ops, List<Variable> adt_vars, List<Axiom> adt_axioms, Equation equation, List<Tree> trees) { this.adt_sorts = adt_sorts; @@ -37,7 +39,26 @@ namespace Eingabeverwaltung.Parser fixedVars = new List<Variable>(); errors = new List<SemanticAnalysisError>(); warnings = new List<SemanticAnalysisWarning>(); - } + } + + /// <summary> + /// Closes the Listener_Helper printing all errors and warnings + /// </summary> + public void close() + { + string errorMessage = "Errors:\r\n"; + foreach(SemanticAnalysisError error in errors) + errorMessage += error.message+"\r\n"; + string warningMessage = "Warnings:\r\n"; + foreach(SemanticAnalysisWarning warning in warnings) + warningMessage += warning.message + "\r\n"; + if (errors.Count != 0) + if (warnings.Count != 0) throw new Exception(errorMessage+warningMessage); + else throw new Exception(errorMessage); + // TODO: How warnings? + // print warnings in Ausgabeverwalter of ProgramForHuman / ProgramForYapex + } + // Equation public void EnterEq() { @@ -53,6 +74,7 @@ namespace Eingabeverwaltung.Parser errors.Add(new SemanticAnalysisError(coords, "Calculated " + trees.Count + " Trees in Equation! The Trees are: " + TreeListToString(trees))); while (trees.Count < 2) trees.Add(null); + } equation = new Equation(trees[0], trees[1], adt_vars); } @@ -100,7 +122,7 @@ namespace Eingabeverwaltung.Parser Operation operation = findOperationInADT_Ops(treeName, childCount,coords); if (operation == null) throw new SemanticAnalysisDeadlyError(coords,"The Tree " + treeName + " could not be found in Operations of the ADT!"); // deadly because how much trees to remove from trees then? List<Tree> children = new List<Tree>(); - for (int i = 0; i < operation.sorts.Count - 1; i++) + for (int i = 0; i < childCount; i++) // childCount because to better coordinate with the input { if (trees.Count == 0) { @@ -113,7 +135,7 @@ namespace Eingabeverwaltung.Parser trees.RemoveAt(trees.Count - 1); } children.Reverse(); - Test_ComposedTree_Children_Sorts_are_correct(operation, children); + Test_ComposedTree_Children_Sorts_are_correct(operation, children,coords); Tree currentTree = new ComposedTree(coords, operation, children); trees.Add(currentTree); } @@ -124,7 +146,6 @@ namespace Eingabeverwaltung.Parser /// </summary> /// <param name="treeName"></param> /// <param name="coords"></param> - /// <exception cref="KontextException"></exception> public void ExitFTreeBez(string treeName, Coords coords) { Tree result = null; @@ -146,6 +167,7 @@ namespace Eingabeverwaltung.Parser /// ExitFTreeRoot builds the next incomplete Composed Tree. /// </summary> /// <param name="coords"></param> + /// <exception cref="SemanticAnalysisDeadlyError"> </exception> public void ExitFTreeRoot(Coords coords) { for (int rootPos = trees.Count - 1; rootPos>= 0; rootPos--) @@ -323,9 +345,9 @@ namespace Eingabeverwaltung.Parser private void Test_ComposedTree_ChildCount_is_corrent(Operation operation, int inputtedChildCount, Coords coords) { if (operation.sorts.Count != inputtedChildCount + 1) - throw new KontextException(coords,"The Operation_Tree " + operation.name + " was inputted with " + inputtedChildCount + " children, expected " + (operation.sorts.Count - 1) + " children!"); + errors.Add(new SemanticAnalysisError(coords,"The Operation_Tree " + operation.name + " was inputted with " + inputtedChildCount + " children, expected " + (operation.sorts.Count - 1) + " children!")); } - private void Test_ComposedTree_Children_Sorts_are_correct(Operation operation, List<Tree> children) => Test_ComposedTree_Children_Sorts_are_correct(operation, children, new Coords(-1,-1)); + private void Test_ComposedTree_Children_Sorts_are_correct(Operation operation, List<Tree> children, Coords coords) { for (int i = 0; i < children.Count; i++) @@ -333,8 +355,11 @@ namespace Eingabeverwaltung.Parser string type = ""; if (children[i] is ComposedTree) type = "ComposedTree"; else if (children[i] is TreeVariable) type = "Variable"; - else if (children[i] == null) { errors.Add(new SemanticAnalysisError(coords, "The child number "+i+" of the tree "+operation.name+" is null.")); continue; } + else if (children[i] == null) { if (errors.Count == 0) errors.Add(new SemanticAnalysisError(coords, "The child number "+i+" of the tree "+operation.name+" is null.")); continue; } else throw new SemanticAnalysisDeadlyError(coords, "Found a Tree " + children[i].name + " that is neither TreeVariable nor ComposedTree!"); + if (children[i].sort == null) { if (errors.Count == 0) errors.Add(new SemanticAnalysisError(coords, "The sort child number " + i + " of the tree " + operation.name + " is null.")); continue; } + if (operation.sorts[i] == null) { if (errors.Count == 0) errors.Add(new SemanticAnalysisError(coords, "The sort child number " + i + " of the operation " + operation.name + " is null.")); continue; } + if (operation == null) Console.WriteLine("operation is null "); if (children[i].sort != operation.sorts[i]) errors.Add(new SemanticAnalysisError(coords, "Error while building the tree " + operation.name + ": The the child (" + type + ") " + children[i].name + " with the Sort " + children[i].sort.name + " is not " + operation.sorts[i].name + "!")); @@ -353,7 +378,7 @@ namespace Eingabeverwaltung.Parser { if (leftTree.sort.name != rightTree.sort.name) errors.Add(new SemanticAnalysisError(coords, "The Equation has not the same Sort on its 2 sides! Sort of leftTree: " + leftTree.sort.name + " Sort of rightTree: " + rightTree.sort.name)); - }catch(NullReferenceException) { errors.Add(new SemanticAnalysisError(coords, "One or more sides of one Equation are null!")); } + }catch(NullReferenceException n) { errors.Add(new SemanticAnalysisError(coords, "One or more sides of one Equation are null!")); } } /// <summary> diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/SimpleEingabeverwalter.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/SimpleEingabeverwalter.cs index 2f9f0a9..6622f5f 100644 --- a/BewerterStrukturellerInduktion/Eingabeverwaltung/SimpleEingabeverwalter.cs +++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/SimpleEingabeverwalter.cs @@ -7,7 +7,7 @@ using System.Text; namespace Eingabeverwaltung { - public class SimpleEingabeverwalter : AbstactEingabeverwalter + public class SimpleEingabeverwalter : AbstractEingabeverwalter { private string adtPath; private string taskPath; diff --git a/BewerterStrukturellerInduktion/Eingabeverwaltung/TestEingabeverwalter.cs b/BewerterStrukturellerInduktion/Eingabeverwaltung/TestEingabeverwalter.cs new file mode 100644 index 0000000..a1ae3a0 --- /dev/null +++ b/BewerterStrukturellerInduktion/Eingabeverwaltung/TestEingabeverwalter.cs @@ -0,0 +1,60 @@ + + +using Eingabeverwaltung.Metamodell; +using Eingabeverwaltung.Parser; +using System.Collections.Generic; +using System.Collections.Immutable; +using System; +using System.IO; + +namespace Eingabeverwaltung +{ + /// <summary> + /// TestEingabeverwalter lets you managing the input and the exceptions thrown while parsing. + /// </summary> + public class TestEingabeverwalter : AbstractEingabeverwalter + { + public TestEingabeverwalter() :base() { } + + /// <summary> + /// All Tests are managing its input on their own, they need to call each input file on their own + /// </summary> + /// <exception cref="InvalidOperationException"></exception> + public override void verwalteEingabe() + { + throw new InvalidOperationException(); + } + + /// <summary> + /// This is only for Testing. All Exceptions + /// </summary> + /// <param name="action"></param> + /// <param name="path"></param> + public void Eingabe_Interface(string action, string path) + { + ImmutableDictionary<string, Action<string>> eingabe = new Dictionary<string, Action<string>> + { + ["ADT"] = ADT_Eingabe, + ["Task"] = Task_Eingabe, + ["Proof"] = Proof_Eingabe, + }.ToImmutableDictionary(); + string input = File.ReadAllText(path); + eingabe[action](input); + void ADT_Eingabe(string input) + { + ADT adt = ADT_Antlr.parse(input); + inputContainer = new Container(); + inputContainer.ADT = adt; + } + void Task_Eingabe(string input) + { + Task_Antlr.parse(input, inputContainer); + inputContainer.Proof = null; + } + void Proof_Eingabe(string input) + { + Proof_Antlr.parse(input,inputContainer); + } + } + } +} diff --git a/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs b/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs index a2e0dab..d8fb3c7 100644 --- a/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs +++ b/BewerterStrukturellerInduktion/Testverwaltung/ExtraTest.cs @@ -1,4 +1,7 @@ -using Ueberpruefung; +using System; +using System.Collections.Generic; +using System.IO; +using Ueberpruefung; namespace Testverwaltung { @@ -7,7 +10,6 @@ namespace Testverwaltung private int currentTestNumber; public ExtraTest() : base() { - numTests = 2; currentTestNumber = 0; } public override bool run() @@ -16,6 +18,8 @@ namespace Testverwaltung string pathPrefix = "Tests\\extra\\"; singleTest(pathPrefix+"FTree\\"); singleTest(pathPrefix+"Comment\\"); + NonDeadSemErrsTest(pathPrefix + "NonDeadSemErrs\\"); + numTests = currentTestNumber; return passed; } @@ -27,5 +31,42 @@ namespace Testverwaltung Ueberpruefer.ueberpruefe(ein.GetContainer()); resultString += assert(currentTestNumber++, aus.NoErrors(), aus.printAllErrors(ein.GetContainer())); } + + /// <summary> + /// Tests Exceptions of non dead semantic errors + /// </summary> + /// <param name="path"></param> + private void NonDeadSemErrsTest(string path) + { + List<string> adtFileNames = new List<string>() { "tree1","tree2","tree3","tree4","tree5","sort","op","ax","chaos" }; + List<string> adtShallValues = new List<string>() + { + "Errors:\r\nError in 9:11: The Operation_Tree plus was inputted with 1 children, expected 2 children!\r\nError in 10:11: The Operation_Tree plus was inputted with 3 children, expected 2 children!\r\n", + "Error in 10:18: The Tree ink could not be found in Operations of the ADT!", + "Errors:\r\nError in 9:18: The Tree zero could not be found in Vars or Operations of the ADT!\r\nError in 9:26: The Tree k could not be found in Vars or Operations of the ADT!\r\nError in 9:7: One or more sides of one Equation are null!\r\nError in 10:22: The Tree k could not be found in Vars or Operations of the ADT!\r\n", + "Errors:\r\nError in 9:11: Error while building the tree plus: The the child (Variable) k with the Sort Nat2 is not Nat!\r\nError in 9:7: The Equation has not the same Sort on its 2 sides! Sort of leftTree: Nat Sort of rightTree: Nat2\r\nError in 11:7: The Equation has not the same Sort on its 2 sides! Sort of leftTree: Nat2 Sort of rightTree: Nat\r\nError in 12:27: Error while building the tree plus: The the child (ComposedTree) mal with the Sort Nat2 is not Nat!\r\nError in 12:7: The Equation has not the same Sort on its 2 sides! Sort of leftTree: Nat2 Sort of rightTree: Nat\r\n", + "Errors:\r\nError in 8:23: The Variable n was defined more than 1 times.!\r\n", + "Errors:\r\nError in 4:11: The Sort Nat was defined more than 1 times in Sorts of ADT!\r\nError in 5:0: The sort Nat has building constructors, but no basic constructors.\r\n", + "Errors:\r\nError in 7:24: Found a Sort Nat2 in Operations that was not defined in Sorts!\r\nError in 7:11: The Operation null was defined more than 1 times in Operations of ADT!\r\n", + "Errors:\r\nError in 9:7: The Axiom p0 was defined more than 1 times in Axioms of ADT!\r\n", + "Errors:\r\nError in 4:11: The Sort Nat was defined more than 1 times in Sorts of ADT!\r\nError in 5:18: Found a Sort Blub in Operations that was not defined in Sorts!\r\nError in 8:17: Found a Sort Nat1 in Operations that was not defined in Sorts!\r\nError in 8:25: Found a Sort Nat2 in Operations that was not defined in Sorts!\r\nError in 8:33: Found a Sort Blub in Operations that was not defined in Sorts!\r\nError in 9:11: The Operation plus was defined more than 1 times in Operations of ADT!\r\nError in 10:17: Found a Sort Blub in Operations that was not defined in Sorts!\r\nError in 10:25: Found a Sort Nat3 in Operations that was not defined in Sorts!\r\nError in 10:33: Found a Sort Nat4 in Operations that was not defined in Sorts!\r\nError in 13:5: Found a Sort Bla in Variable that was not defined in Sorts!\r\nError in 13:14: Found a Sort Nat5 in Variable that was not defined in Sorts!\r\nError in 13:24: Found a Sort Bla2 in Variable that was not defined in Sorts!\r\nError in 13:24: The Variable n was defined more than 1 times.!\r\nError in 16:18: The Tree null could not be found in Vars or Operations of the ADT!\r\nError in 16:7: One or more sides of one Equation are null!\r\nError in 17:7: One or more sides of one Equation are null!\r\nError in 18:17: The Tree null could not be found in Vars or Operations of the ADT!\r\nError in 18:25: The Tree null could not be found in Vars or Operations of the ADT!\r\nError in 18:7: One or more sides of one Equation are null!\r\nError in 19:7: One or more sides of one Equation are null!\r\n" + }; + for (int i = 0; i < adtFileNames.Count; i++) + ExceptionTesting("ADT", path + adtFileNames[i]+".adt", adtShallValues[i]); + } + + private void ExceptionTesting(string inputType, string inputPath, string shallMessage) + { + string ExceptionMessage = ""; + try + { + ein.Eingabe_Interface(inputType, inputPath); + } + catch (System.Exception e) + { + ExceptionMessage = e.Message; + } + resultString += assert(currentTestNumber++, shallMessage, ExceptionMessage); + } } } diff --git a/BewerterStrukturellerInduktion/Testverwaltung/Test.cs b/BewerterStrukturellerInduktion/Testverwaltung/Test.cs index 4a40333..2ce4723 100644 --- a/BewerterStrukturellerInduktion/Testverwaltung/Test.cs +++ b/BewerterStrukturellerInduktion/Testverwaltung/Test.cs @@ -8,13 +8,13 @@ namespace Testverwaltung protected string resultString; protected int numTests; protected bool passed; - protected Eingabeverwalter ein; + protected TestEingabeverwalter ein; protected Ausgabeverwalter aus; public Test() { resultString = ""; - ein = new Eingabeverwalter(); + ein = new TestEingabeverwalter(); aus = new Ausgabeverwalter(); passed = true; } diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.adt b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.adt new file mode 100644 index 0000000..038c96c --- /dev/null +++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/0riginal.adt @@ -0,0 +1,11 @@ +name Peano +sorts Nat +constructors null: Nat + inc: Nat -> Nat +operations plus: Nat >< Nat -> Nat + mal: Nat >< Nat -> Nat +vars n : Nat, m : Nat +axioms p0: plus(n,null) = n + p1: plus(n,inc(m)) = inc(plus(n,m)) + m0: mal(n,null) = null + m1: mal(n,inc(m)) = plus(mal(n,m),n) \ No newline at end of file diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/ax.adt b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/ax.adt new file mode 100644 index 0000000..37b33bb --- /dev/null +++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/ax.adt @@ -0,0 +1,11 @@ +name Peano +sorts Nat +constructors null: Nat + inc: Nat -> Nat +operations plus: Nat >< Nat -> Nat + mal: Nat >< Nat -> Nat +vars n : Nat, m : Nat +axioms p0: plus(n,null) = n + p0: plus(n,inc(m)) = inc(plus(n,m)) + m0: mal(n,null) = null + m1: mal(n,inc(m)) = plus(mal(n,m),n) \ No newline at end of file diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/chaos.adt b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/chaos.adt new file mode 100644 index 0000000..ea053cc --- /dev/null +++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/chaos.adt @@ -0,0 +1,19 @@ +name Peano_AllErrorsTogether +// sorts with building and without basic constructors +// multiple sorts with same name +sorts Nat, Nat +constructors inc: Blub -> Nat +// multiple operations with same name +// operation has sorts undefined in adt +operations plus: Nat1 >< Nat2 -> Blub + plus: Nat + mal: Blub >< Nat3 -> Nat4 +// variable has sorts undefined in adt +// multiple variables defined with same name +vars n : Bla, m : Nat5, n: Bla2 +// Equation with wrong sorts +// Trees with wrong sorts +axioms p0: plus(n,null) = n + p1: plus(n,inc(m)) = inc(plus(n,m)) + m0: mal(n,null) = null + m1: mal(n,inc(m)) = plus(mal(n,m),n) \ No newline at end of file diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/op.adt b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/op.adt new file mode 100644 index 0000000..37a1957 --- /dev/null +++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/op.adt @@ -0,0 +1,12 @@ +name Peano +sorts Nat +constructors null: Nat + inc: Nat -> Nat +operations plus: Nat >< Nat -> Nat + mal: Nat >< Nat -> Nat + null: Nat -> Nat2 +vars n : Nat, m : Nat +axioms p0: plus(n,null) = n + p1: plus(n,inc(m)) = inc(plus(n,m)) + m0: mal(n,null) = null + m1: mal(n,inc(m)) = plus(mal(n,m),n) \ No newline at end of file diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/sort.adt b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/sort.adt new file mode 100644 index 0000000..0ff96c3 --- /dev/null +++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/sort.adt @@ -0,0 +1,13 @@ +name Peano +// multiple sorts with same name +// sort with building, but without basic constructor +sorts Nat, Nat +constructors inc: Nat -> Nat +operations plus: Nat >< Nat -> Nat + mal: Nat >< Nat -> Nat + null: Nat +vars n : Nat, m : Nat +axioms p0: plus(n,null) = n + p1: plus(n,inc(m)) = inc(plus(n,m)) + m0: mal(n,null) = null + m1: mal(n,inc(m)) = plus(mal(n,m),n) \ No newline at end of file diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree1.adt b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree1.adt new file mode 100644 index 0000000..0ef811b --- /dev/null +++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree1.adt @@ -0,0 +1,12 @@ +name Peano +sorts Nat +constructors null: Nat + inc: Nat -> Nat +operations plus: Nat >< Nat -> Nat + mal: Nat >< Nat -> Nat +vars n : Nat, m : Nat +// tree wrong child count +axioms p0: plus(n) = n + p1: plus(n,inc(m),null) = inc(plus(n,m)) + m0: mal(n,null) = null + m1: mal(n,inc(m)) = plus(mal(n,m),n) \ No newline at end of file diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree2.adt b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree2.adt new file mode 100644 index 0000000..b34b51b --- /dev/null +++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree2.adt @@ -0,0 +1,12 @@ +name Peano +sorts Nat +constructors null: Nat + inc: Nat -> Nat +operations plus: Nat >< Nat -> Nat + mal: Nat >< Nat -> Nat +vars n : Nat, m : Nat +// composed tree names undefined in operation (deadly) +axioms p0: plus(n,null) = n + p1: plus(n,ink(m)) = inc(plus(n,m)) + m0: mal(n,null) = null + m1: mal(n,inc(m)) = plus(mal(n,m),n) \ No newline at end of file diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree3.adt b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree3.adt new file mode 100644 index 0000000..8283717 --- /dev/null +++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree3.adt @@ -0,0 +1,12 @@ +name Peano +sorts Nat +constructors null: Nat + inc: Nat -> Nat +operations plus: Nat >< Nat -> Nat + mal: Nat >< Nat -> Nat +vars n : Nat, m : Nat +// tree-leaf names undefined in operation or variables +axioms p0: plus(n,zero) = k + p1: plus(n,inc(k)) = inc(plus(n,m)) + m0: mal(n,null) = null + m1: mal(n,inc(m)) = plus(mal(n,m),n) \ No newline at end of file diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree4.adt b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree4.adt new file mode 100644 index 0000000..217ae97 --- /dev/null +++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree4.adt @@ -0,0 +1,12 @@ +name Peano +sorts Nat, Nat2 +constructors null: Nat + inc: Nat -> Nat +operations plus: Nat >< Nat -> Nat + mal: Nat >< Nat -> Nat2 +vars n : Nat, m : Nat, k : Nat2 +// wrong sorts in trees and equation +axioms p0: plus(k,null) = k + p1: plus(n,inc(m)) = inc(plus(n,m)) + m0: mal(n,null) = null + m1: mal(n,inc(m)) = plus(mal(n,m),n) \ No newline at end of file diff --git a/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree5.adt b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree5.adt new file mode 100644 index 0000000..3cd4046 --- /dev/null +++ b/BewerterStrukturellerInduktion/bin/Debug/netcoreapp5.0/Tests/extra/NonDeadSemErrs/tree5.adt @@ -0,0 +1,12 @@ +name Peano +sorts Nat, Nat2 +constructors null: Nat + inc: Nat -> Nat +operations plus: Nat >< Nat -> Nat + mal: Nat >< Nat -> Nat +// variable defined multiple times +vars n : Nat, m : Nat, n : Nat2 +axioms p0: plus(n,null) = n + p1: plus(n,inc(m)) = inc(plus(n,m)) + m0: mal(n,null) = null + m1: mal(n,inc(m)) = plus(mal(n,m),n) \ No newline at end of file -- GitLab