diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index d90a738ff3d..32c67b64e4b 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -275,6 +275,7 @@ MAP_UPDATE: '\\map_update'; //KeY extension, not official JML MAX: '\\max'; E_MEASURED_BY: '\\measured_by' -> type(MEASURED_BY); MIN: '\\min'; +MSET: '\\msetRange'; //KeY extension, not official JML NEWELEMSFRESH: '\\new_elems_fresh'; //KeY extension, not official JML NEW_OBJECTS: '\\new_objects'; //KeY extension, not official JML NONNULLELEMENTS: '\\nonnullelements'; diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index aed3866b353..275820bd243 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -356,6 +356,7 @@ jmlprimary | java_math_expression #primaryJavaMathExpression | beforeexpression #pignore6 | transactionUpdated #pignore7 + | msetrangeterm #pignore8 | BACKUP LPAREN expression RPAREN #primaryBackup | PERMISSION LPAREN expression RPAREN #primaryPermission | NONNULLELEMENTS LPAREN expression RPAREN #primaryNNE @@ -426,6 +427,7 @@ safe_math_expression: (SAFE_MATH LPAREN expression RPAREN); bigint_math_expression: (BIGINT_MATH LPAREN expression RPAREN); beforeexpression: (BEFORE LPAREN expression RPAREN); bsumterm: LPAREN BSUM quantifiedvardecls SEMI (expression SEMI expression SEMI expression) RPAREN; +msetrangeterm: LPAREN MSET quantifiedvardecls SEMI (expression SEMI expression SEMI expression) RPAREN; seqdefterm: LPAREN SEQDEF quantifiedvardecls SEMI (expression SEMI expression SEMI expression) RPAREN; quantifiedvardecls: typespec quantifiedvariabledeclarator (COMMA quantifiedvariabledeclarator)*; boundvarmodifiers: (NON_NULL | NULLABLE); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java index 6dfc71cd6e1..fa74ce98dc6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java @@ -116,6 +116,10 @@ public SeqLDT getSeqLDT() { return (SeqLDT) getLDT(SeqLDT.NAME); } + public MSetLDT getMSetLDT() { + return (MSetLDT) getLDT(MSetLDT.NAME); + } + public SortLDT getSortLDT() { return (SortLDT) getLDT(SortLDT.NAME); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/PrimitiveType.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/PrimitiveType.java index 28cf6fe9942..25d3f7f8e34 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/PrimitiveType.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/PrimitiveType.java @@ -9,7 +9,6 @@ import java.util.Map; import de.uka.ilkd.key.java.ast.expression.literal.*; -import de.uka.ilkd.key.java.ast.expression.literal.Literal; import de.uka.ilkd.key.ldt.*; import de.uka.ilkd.key.logic.ProgramElementName; @@ -59,6 +58,8 @@ public final class PrimitiveType implements Type { new PrimitiveType("\\map", EmptyMapLiteral.INSTANCE, MapLDT.NAME); public static final PrimitiveType JAVA_TYPE = new PrimitiveType("\\TYPE", NullLiteral.NULL, SortLDT.NAME); + public static final PrimitiveType JAVA_MSET = + new PrimitiveType("\\mset", EmptyMSetLiteral.INSTANCE, MSetLDT.NAME); public static final PrimitiveType PROGRAM_SV = new PrimitiveType("SV", null, null); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java new file mode 100644 index 00000000000..6746a885cd3 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java @@ -0,0 +1,42 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.literal; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.ldt.MSetLDT; + +import org.key_project.logic.Name; + +public non-sealed class EmptyMSetLiteral extends Literal { + public static final EmptyMSetLiteral INSTANCE = new EmptyMSetLiteral(); + + private EmptyMSetLiteral() {} + + @Override + public boolean equals(Object o) { + return o == this; + } + + @Override + protected int computeHashCode() { + return System.identityHashCode(this); + } + + public void visit(Visitor v) { + v.performActionOnEmptyMSetLiteral(this); + } + + + public KeYJavaType getKeYJavaType(Services javaServ) { + return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_MSET); + } + + @Override + public Name getLDTName() { + return MSetLDT.NAME; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptySeqLiteral.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptySeqLiteral.java index 9045dd67f09..fbf8251356c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptySeqLiteral.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptySeqLiteral.java @@ -33,7 +33,6 @@ public void visit(Visitor v) { v.performActionOnEmptySeqLiteral(this); } - public KeYJavaType getKeYJavaType(Services javaServ) { return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_SEQ); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java index b933c076c6e..13424e43a3f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java @@ -40,9 +40,9 @@ class Literal extends JavaProgramElement implements Expression, TerminalProgramElement - permits AbstractIntegerLiteral, BooleanLiteral, DoubleLiteral, EmptyMapLiteral, - EmptySeqLiteral, EmptySetLiteral, FloatLiteral, FreeLiteral, NullLiteral, RealLiteral, - StringLiteral { + permits AbstractIntegerLiteral, BooleanLiteral, DoubleLiteral, EmptyMSetLiteral, + EmptyMapLiteral, EmptySeqLiteral, EmptySetLiteral, FloatLiteral, FreeLiteral, NullLiteral, + RealLiteral, StringLiteral { public Literal(@Nullable PositionInfo pi, @Nullable List comments) { super(pi, comments); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetCard.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetCard.java new file mode 100644 index 00000000000..8caf741db18 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetCard.java @@ -0,0 +1,49 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.ast.expression.Operator; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + +public class MSetCard extends Operator { + + public MSetCard(ExtList children) { + super(children); + } + + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public void visit(Visitor v) { + v.performActionOnMSetCard(this); + } + + + @Override + public int getArity() { + return 1; + } + + + @Override + public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) { + return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_INT); + } + + + @Override + public int getNotation() { + return Operator.PREFIX; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetDiff.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetDiff.java new file mode 100644 index 00000000000..0de27b61292 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetDiff.java @@ -0,0 +1,38 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + + +public class MSetDiff extends BinaryOperator { + public MSetDiff(ExtList children) { + super(children); + } + + public MSetDiff(Expression msetA, Expression msetB) { + super(msetA, msetB); + } + + + + @Override + public void visit(Visitor v) { + v.performActionOnMSetDiff(this); + } + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public int getNotation() { + return PREFIX; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetIntersect.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetIntersect.java new file mode 100644 index 00000000000..fa3d12c41d9 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetIntersect.java @@ -0,0 +1,39 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + +public class MSetIntersect extends BinaryOperator { + + + public MSetIntersect(ExtList children) { + super(children); + } + + public MSetIntersect(Expression msetA, Expression msetB) { + super(msetA, msetB); + } + + + + @Override + public void visit(Visitor v) { + v.performActionOnMSetIntersect(this); + } + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public int getNotation() { + return PREFIX; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetMul.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetMul.java new file mode 100644 index 00000000000..512eda0d16f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetMul.java @@ -0,0 +1,50 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.ast.expression.Operator; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + + +public class MSetMul extends Operator { + + public MSetMul(ExtList children) { + super(children); + } + + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public void visit(Visitor v) { + v.performActionOnMSetMul(this); + } + + @Override + public int getArity() { + return 1; + } + + + @Override + public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) { + return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_INT); + } + + + @Override + public int getNotation() { + return Operator.PREFIX; + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSingle.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSingle.java new file mode 100644 index 00000000000..36872fcaba2 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSingle.java @@ -0,0 +1,43 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.Operator; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + +public class MSetSingle extends Operator { + + public MSetSingle(ExtList children) { super(children); } + + public MSetSingle(Expression child) { super(child); } + + public int getPrecedence() { + return 0; + } + + + public int getNotation() { + return PREFIX; + } + + + public void visit(Visitor v) { + v.performActionOnMSetSingle(this); + } + + public int getArity() { + return 1; + } + + public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) { + return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_MSET); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSum.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSum.java new file mode 100644 index 00000000000..78ec802d3c6 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSum.java @@ -0,0 +1,38 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + +public class MSetSum extends BinaryOperator { + + public MSetSum(ExtList children) { + super(children); + } + + public MSetSum(Expression msetA, Expression msetB) { + super(msetA, msetB); + } + + + + @Override + public void visit(Visitor v) { + v.performActionOnMSetSum(this); + } + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public int getNotation() { + return PREFIX; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetUnion.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetUnion.java new file mode 100644 index 00000000000..78fd39a7005 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetUnion.java @@ -0,0 +1,36 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + +public class MSetUnion extends BinaryOperator { + public MSetUnion(ExtList children) { + super(children); + } + + public MSetUnion(Expression msetA, Expression msetB) { + super(msetA, msetB); + } + + + @Override + public void visit(Visitor v) { + v.performActionOnMSetUnion(this); + } + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public int getNotation() { + return PREFIX; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java index de756e25907..a35e0b3e297 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java @@ -6,7 +6,7 @@ import java.util.ArrayDeque; import java.util.Deque; -import de.uka.ilkd.key.java.*; +import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.declaration.ClassInitializer; import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration; @@ -18,6 +18,8 @@ import de.uka.ilkd.key.java.ast.expression.PassiveExpression; import de.uka.ilkd.key.java.ast.expression.operator.*; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.MSetSum; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.op.IProgramVariable; @@ -1479,6 +1481,92 @@ ProgramElement createNewElement(ExtList changeList) { def.doAction(x); } + public void performActionOnMSetUnion(MSetUnion x) { + + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + + return new MSetUnion(changeList); + } + + }; + + def.doAction(x); + + } + + @Override + public void performActionOnMSetIntersect(MSetIntersect x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetIntersect(changeList); + } + }; + def.doAction(x); + } + + @Override + public void performActionOnMSetSum(MSetSum x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetSum(changeList); + } + }; + def.doAction(x); + + } + + @Override + public void performActionOnMSetDiff(MSetDiff x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetDiff(changeList); + } + }; + def.doAction(x); + + + } + + @Override + public void performActionOnMSetSingle(MSetSingle x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetSingle(changeList); + } + }; + def.doAction(x); + } + + @Override + public void performActionOnMSetCard(MSetCard x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetCard(changeList); + } + }; + def.doAction(x); + } + + @Override + public void performActionOnMSetMul(MSetMul x) { + + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetMul(changeList); + } + }; + def.doAction(x); + } + + @Override public void performActionOnDLEmbeddedExpression(final DLEmbeddedExpression x) { DefaultAction def = new DefaultAction(x) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java index 91bd808e2f8..8bd89a3122e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.visitor; -import de.uka.ilkd.key.java.*; +import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.ccatch.*; import de.uka.ilkd.key.java.ast.declaration.*; @@ -12,17 +12,12 @@ import de.uka.ilkd.key.java.ast.expression.PassiveExpression; import de.uka.ilkd.key.java.ast.expression.literal.*; import de.uka.ilkd.key.java.ast.expression.operator.*; -import de.uka.ilkd.key.java.ast.expression.operator.Subtype; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.*; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.ProgramElementName; -import de.uka.ilkd.key.logic.op.IProgramMethod; -import de.uka.ilkd.key.logic.op.IProgramVariable; -import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.ProgramConstant; -import de.uka.ilkd.key.logic.op.ProgramSV; -import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.AbstractProgramElement; import de.uka.ilkd.key.rule.metaconstruct.ProgramTransformer; import de.uka.ilkd.key.speclang.BlockContract; @@ -190,6 +185,8 @@ public void performActionOnSetUnion(SetUnion x) { doDefaultAction(x); } + + @Override public void performActionOnIntersect(Intersect x) { doDefaultAction(x); @@ -240,6 +237,32 @@ public void performActionOnSeqPut(SeqPut x) { doDefaultAction(x); } + @Override + public void performActionOnEmptyMSetLiteral(EmptyMSetLiteral x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetUnion(MSetUnion x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetIntersect(MSetIntersect x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetSum(MSetSum x) { + doDefaultAction(x); + } + + @Override + public void performActionOnMSetDiff(MSetDiff x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetSingle(MSetSingle x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetMul(MSetMul x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetCard(MSetCard x) { doDefaultAction(x); } + @Override public void performActionOnDLEmbeddedExpression(DLEmbeddedExpression x) { doDefaultAction(x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java index e5299c49298..7b61264883c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.java.ast.expression.operator.*; import de.uka.ilkd.key.java.ast.expression.operator.Subtype; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.*; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.ProgramElementName; @@ -62,6 +63,8 @@ public interface Visitor { void performActionOnSetUnion(SetUnion x); + + void performActionOnIntersect(Intersect x); void performActionOnSetMinus(SetMinus x); @@ -84,6 +87,22 @@ public interface Visitor { void performActionOnSeqPut(SeqPut seqPut); + void performActionOnMSetUnion(MSetUnion x); + + void performActionOnMSetIntersect(MSetIntersect x); + + void performActionOnMSetSum(MSetSum x); + + void performActionOnMSetDiff(MSetDiff x); + + void performActionOnEmptyMSetLiteral(EmptyMSetLiteral x); + + void performActionOnMSetSingle(MSetSingle x); + + void performActionOnMSetMul(MSetMul x); + + void performActionOnMSetCard(MSetCard x); + void performActionOnDLEmbeddedExpression(DLEmbeddedExpression x); void performActionOnStringLiteral(StringLiteral x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java index fe11de64b3b..98d33b14a78 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java @@ -154,6 +154,7 @@ public static Map getNewLDTInstances(Services s) { ret.put(DoubleLDT.NAME, new DoubleLDT(s)); ret.put(RealLDT.NAME, new RealLDT(s)); ret.put(CharListLDT.NAME, new CharListLDT(s)); + ret.put(MSetLDT.NAME, new MSetLDT(s)); return ret; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java new file mode 100644 index 00000000000..0ef9fdae04e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java @@ -0,0 +1,187 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.ldt; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.Type; +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.Operator; +import de.uka.ilkd.key.java.ast.expression.literal.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.*; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.logic.GenericArgument; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.TermServices; + +import de.uka.ilkd.key.logic.op.ParametricFunctionDecl; +import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; +import org.key_project.logic.Name; +import org.key_project.logic.op.Function; +import org.key_project.logic.sort.Sort; +import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableList; + +public class MSetLDT extends LDT { + + public static final Name NAME = new Name("Mset"); + + private final ParametricFunctionDecl msetRange; + private final ParametricFunctionDecl msetEmpty; + private final ParametricFunctionDecl msetSingle; + private final ParametricFunctionDecl msetSum; + private final ParametricFunctionDecl msetDiff; + private final Function msetCard; + private final Function msetMul; + + public MSetLDT(TermServices services) { + super(NAME, services); + msetMul = addFunction(services, "msetMul"); + msetEmpty = addParametricFunction(services, "msetEmpty"); + msetSingle = addParametricFunction(services, "msetSingle"); + msetSum = addParametricFunction(services, "msetSum"); + msetDiff = addParametricFunction(services, "msetDiff"); + msetCard = addFunction(services, "msetCard"); + msetRange = addParametricFunction(services, "msetRange"); + } + + + public ParametricFunctionDecl getMsetRange() { return msetRange; } + + /** + * Returns the select function for the given sort. + */ + public ParametricFunctionInstance getMsetRange(Sort instanceSort, TermServices services) { + return ParametricFunctionInstance.get(msetRange, + ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); + } + + + public Function getMsetMul() { + return msetMul; + } + + public ParametricFunctionDecl getMsetEmpty() { + return msetEmpty; + } + + /** + * Returns the select function for the given sort. + */ + public ParametricFunctionInstance getMsetEmpty(Sort instanceSort, TermServices services) { + return ParametricFunctionInstance.get(msetEmpty, + ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); + } + + + public ParametricFunctionDecl getMsetSingle() { + return msetSingle; + } + + /** + * Returns the select function for the given sort. + */ + public ParametricFunctionInstance getMsetSingle(Sort instanceSort, TermServices services) { + return ParametricFunctionInstance.get(msetSingle, + ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); + } + + public ParametricFunctionDecl getMsetSum() { + return msetSum; + } + + /** + * Returns the select function for the given sort. + */ + public ParametricFunctionInstance getMsetSum(Sort instanceSort, TermServices services) { + return ParametricFunctionInstance.get(msetSum, + ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); + } + + + + public ParametricFunctionDecl getMsetDiff() { + return msetDiff; + } + + /** + * Returns the select function for the given sort. + */ + public ParametricFunctionInstance getMsetDiff(Sort instanceSort, TermServices services) { + return ParametricFunctionInstance.get(msetDiff, + ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); + } + + @Override + public boolean isResponsible(Operator op, JTerm[] subs, Services services, + ExecutionContext ec) { + return op instanceof MSetCard || op instanceof MSetMul + || op instanceof de.uka.ilkd.key.java.ast.expression.operator.mst.MSetSingle + || op instanceof MSetIntersect || + op instanceof MSetDiff || op instanceof MSetUnion || op instanceof MSetSum; + } + + @Override + public boolean isResponsible(Operator op, JTerm left, JTerm right, Services services, + ExecutionContext ec) { + return op instanceof MSetUnion || op instanceof MSetIntersect + || op instanceof de.uka.ilkd.key.java.ast.expression.operator.mst.MSetSum + || op instanceof MSetDiff; + } + + @Override + public boolean isResponsible(Operator op, JTerm sub, TermServices services, + ExecutionContext ec) { + return op instanceof MSetSingle || op instanceof MSetMul || op instanceof MSetCard; + } + + @Override + public JTerm translateLiteral(Literal lit, Services services) { + throw new RuntimeException("Not implemented yet"); +// assert lit instanceof EmptyMSetLiteral; +// return services.getTermBuilder().func(msetEmpty, lit.g); + } + + @Override + public Function getFunctionFor(Operator op, Services services, ExecutionContext ec) { + throw new RuntimeException("Not implemented yet"); + // if (op instanceof MSetSingle) { +// return msetSingle; +// } else if (op instanceof MSetCard) { +// return msetCard; +// } else if (op instanceof MSetUnion) { +// return msetUnion; +// } else if (op instanceof MSetDiff) { +// return msetDiff; +// } else if (op instanceof MSetSum) { +// return msetSum; +// } else if (op instanceof MSetIntersect) { +// return msetIntersec; +// } else if (op instanceof MSetMul) { +// return msetMul; +// } +// +// assert false; +// return null; + } + + @Override + public boolean hasLiteralFunction(Function f) { + return f.equals(msetEmpty); + } + + @Override + public Expression translateTerm(JTerm t, ExtList children, Services services) { + if (t.op().equals(msetEmpty)) { + return EmptyMSetLiteral.INSTANCE; + } + assert false; + return null; + } + + @Override + public Type getType(JTerm t) { + assert false; + return null; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/LexPathOrdering.java b/key.core/src/main/java/de/uka/ilkd/key/logic/LexPathOrdering.java index c6616c6edec..a7ca796a8ce 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/LexPathOrdering.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/LexPathOrdering.java @@ -424,6 +424,13 @@ protected Integer getWeight(Operator p_op) { return 7; } + + if (opStr.equals("msetSingle")) { + return 6; + } + if (opStr.equals("msetSum")) { + return 7; + } return null; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java index 85e309de798..2aec9cc3e47 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java @@ -2164,6 +2164,16 @@ public JTerm seqReverse(JTerm s) { return func(services.getTypeConverter().getSeqLDT().getSeqReverse(), s); } + public JTerm msetEmpty(Sort instanceSort) { + return func(services.getTypeConverter().getMSetLDT().getMsetEmpty(instanceSort, services)); + } + + public JTerm msetRange(QuantifiableVariable qv, JTerm left, JTerm right, JTerm supplier, Sort instanceSort) { + return func(services.getTypeConverter().getMSetLDT().getMsetRange(instanceSort, services), + new JTerm[] { left, right, supplier }, + new ImmutableArray<>(qv)); + } + // ------------------------------------------------------------------------- // misc (moved from key.util.MiscTools) // ------------------------------------------------------------------------- diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java index 535d844ceaa..924642ed9f6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java @@ -56,7 +56,7 @@ /** * This visitor creates expression from {@link de.uka.ilkd.key.nparser.KeyAst.Term}. You should use - * the facade {@link de.uka.ilkd.key.nparser.KeyIO#parseExpression(String)} for term parsing. + * the facade {@link de.uka.ilkd.key.nparser.KeyIO#parseExpression(String)} for JTerm parsing. * * @author weigl */ @@ -64,7 +64,7 @@ public class ExpressionBuilder extends DefaultBuilder { public static final Logger LOGGER = LoggerFactory.getLogger(ExpressionBuilder.class); public static final String NO_HEAP_EXPRESSION_BEFORE_AT_EXCEPTION_MESSAGE = - "Expecting select term before '@', not: "; + "Expecting select JTerm before '@', not: "; /** * The current abbreviation used for resolving "@name" terms. @@ -175,9 +175,9 @@ public static String operatorOfJavaBlock(String raw) { return "n/a"; } - private static boolean isSelectTerm(JTerm term) { - return term.op() instanceof ParametricFunctionInstance pfi - && pfi.getBase().name().toString().equals("select") && term.arity() == 3; + private static boolean isSelectTerm(JTerm JTerm) { + return JTerm.op() instanceof ParametricFunctionInstance pfi + && pfi.getBase().name().toString().equals("select") && JTerm.arity() == 3; } @Override @@ -264,7 +264,7 @@ public JTerm visitConjunction_term(JavaKeYParser.Conjunction_termContext ctx) { t = binaryTerm(ctx, Junctor.AND, t, accept(c)); } return t; - // Term termR = accept(ctx.b); + // JTerm termR = accept(ctx.b); // return binaryTerm(ctx, Junctor.AND, termL, termR); } @@ -427,10 +427,10 @@ public Object visitStrong_arith_term_2(JavaKeYParser.Strong_arith_term_2Context // "mod" : // "div").collect(Collectors.toList()); - JTerm term = accept(ctx.a); - var sort = term.sort(); + JTerm JTerm = accept(ctx.a); + var sort = JTerm.sort(); if (sort == null) { - semanticError(ctx, "No sort for term '%s'", term); + semanticError(ctx, "No sort for JTerm '%s'", JTerm); } var ldt = services.getTypeConverter().getLDTFor(sort); @@ -449,9 +449,9 @@ public Object visitStrong_arith_term_2(JavaKeYParser.Strong_arith_term_2Context semanticError(ctx, "Could not find function symbol '%s' for sort '%s'.", opName, sort); } - term = binaryTerm(ctx, ctx.b.get(i), op, term, termL.get(i)); + JTerm = binaryTerm(ctx, ctx.b.get(i), op, JTerm, termL.get(i)); } - return term; + return JTerm; } protected JTerm capsulateTf(ParserRuleContext ctx, Supplier termSupplier) { @@ -459,8 +459,9 @@ protected JTerm capsulateTf(ParserRuleContext ctx, Supplier termSupplier) } /** - * Builds a term and, on failure, raises a {@link BuildingException} that describes the - * whole term {@code ctx} but is located at {@code locationCtx} (e.g. the offending + * Builds a JTerm and, on failure, raises a {@link BuildingException} that describes + * the + * whole JTerm {@code ctx} but is located at {@code locationCtx} (e.g. the offending * operand of a binary operation rather than the whole expression). */ protected JTerm capsulateTf(ParserRuleContext ctx, ParserRuleContext locationCtx, @@ -469,11 +470,11 @@ protected JTerm capsulateTf(ParserRuleContext ctx, ParserRuleContext locationCtx return termSupplier.get(); } catch (TermCreationException e) { // Surface the actual reason (usually an arity or sort/type mismatch) instead of the - // generic "Could not build term". The TermCreationException message lists the expected + // generic "Could not build JTerm". The TermCreationException message lists the expected // and actual argument sorts, including the sort hashes - these are kept on purpose: // they let one distinguish two different sort objects that share the same name. String reason = e.getMessage() == null ? "" : "\n" + e.getMessage(); - String msg = String.format("Could not type-check term '%s'.%s", ctx.getText(), reason); + String msg = String.format("Could not type-check JTerm '%s'.%s", ctx.getText(), reason); Token at = locationCtx != null ? locationCtx.start : (ctx != null ? ctx.start : null); throw new BuildingException(at, null, msg, e); } @@ -514,7 +515,7 @@ public Object visitBracket_term(JavaKeYParser.Bracket_termContext ctx) { // } /* - * @Override public Term + * @Override public JTerm * visitStatic_attribute_suffix(JavaKeYParser.Static_attribute_suffixContext * ctx) { Operator v = null; String attributeName = * accept(ctx.staticAttributeOrQueryReference()); String className; if @@ -954,16 +955,17 @@ private void markHeapAsExplicit(JTerm a) { } /* - * private Term createStaticAttributeOrMethod(JavaQuery jq, JavaKeYParser.AccesstermContext ctx) + * private JTerm createStaticAttributeOrMethod(JavaQuery jq, JavaKeYParser.AccesstermContext + * ctx) * { * final var kjt = jq.kjt; String mn = jq.attributeNames; if (jq.maybeAttr != null) { * ProgramVariable maybeAttr = getJavaInfo().getAttribute(mn, kjt); if (maybeAttr != null) { var * op = getAttributeInPrefixSort(kjt.getSort(), mn); return createAttributeTerm(null, op, ctx); * } } else { var suffix = ctx.atom_suffix(ctx.atom_suffix().size() - 1); for (IProgramMethod pm * : getJavaInfo().getAllProgramMethods(kjt)) { if (pm != null && pm.isStatic() && - * pm.name().toString().equals(kjt.getFullName() + "::" + mn)) { List arguments = - * mapOf(suffix.attribute_or_query_suffix().result.args.argument()); Term[] args = - * arguments.toArray(new Term[0]); return getJavaInfo().getStaticProgramMethodTerm(mn, args, + * pm.name().toString().equals(kjt.getFullName() + "::" + mn)) { List arguments = + * mapOf(suffix.attribute_or_query_suffix().result.args.argument()); JTerm[] args = + * arguments.toArray(new JTerm[0]); return getJavaInfo().getStaticProgramMethodTerm(mn, args, * kjt.getFullName()); } } } assert false; return null; } */ @@ -1015,10 +1017,10 @@ public Object visitBracket_access_star(JavaKeYParser.Bracket_access_starContext @Override public Object visitBracket_access_indexrange( JavaKeYParser.Bracket_access_indexrangeContext ctx) { - // | term LBRACKET indexTerm=term (DOTRANGE rangeTo=term)? RBRACKET + // | JTerm LBRACKET indexTerm=JTerm (DOTRANGE rangeTo=JTerm)? RBRACKET // #bracket_access_indexrange - JTerm term = pop(); - boolean sequenceAccess = term.sort().name().toString().equalsIgnoreCase("seq"); + JTerm JTerm = pop(); + boolean sequenceAccess = JTerm.sort().name().toString().equalsIgnoreCase("seq"); // boolean heapUpdate = reference.sort().name().toString().equalsIgnoreCase("Heap"); if (sequenceAccess) { @@ -1029,10 +1031,10 @@ public Object visitBracket_access_indexrange( assert indexTerm != null; if (!isIntTerm(indexTerm)) { semanticError(ctx, - "Expecting term of sort %s as index of sequence %s, but found: %s", - IntegerLDT.NAME, term, indexTerm); + "Expecting JTerm of sort %s as index of sequence %s, but found: %s", + IntegerLDT.NAME, JTerm, indexTerm); } - return getServices().getTermBuilder().seqGet(JavaDLTheory.ANY, term, indexTerm); + return getServices().getTermBuilder().seqGet(JavaDLTheory.ANY, JTerm, indexTerm); } if (ctx.rangeTo != null) { @@ -1060,7 +1062,7 @@ public Object visitBracket_access_indexrange( } } JTerm indexTerm = accept(ctx.indexTerm); - return capsulateTf(ctx, () -> getServices().getTermBuilder().dotArr(term, indexTerm)); + return capsulateTf(ctx, () -> getServices().getTermBuilder().dotArr(JTerm, indexTerm)); } @Override @@ -1134,7 +1136,7 @@ public Object visitAbbreviation(JavaKeYParser.AbbreviationContext ctx) { public JTerm visitIfThenElseTerm(JavaKeYParser.IfThenElseTermContext ctx) { JTerm condF = (JTerm) ctx.condF.accept(this); if (condF.sort() != JavaDLTheory.FORMULA) { - semanticError(ctx, "Condition of an \\if-then-else term has to be a formula."); + semanticError(ctx, "Condition of an \\if-then-else JTerm has to be a formula."); } JTerm thenT = (JTerm) ctx.thenT.accept(this); JTerm elseT = (JTerm) ctx.elseT.accept(this); @@ -1149,7 +1151,7 @@ public Object visitIfExThenElseTerm(JavaKeYParser.IfExThenElseTermContext ctx) { List exVars = accept(ctx.bound_variables()); JTerm condF = accept(ctx.condF); if (condF.sort() != JavaDLTheory.FORMULA) { - semanticError(ctx, "Condition of an \\ifEx-then-else term has to be a formula."); + semanticError(ctx, "Condition of an \\ifEx-then-else JTerm has to be a formula."); } JTerm thenT = accept(ctx.thenT); @@ -1325,7 +1327,7 @@ public boolean isClass(String p) { * Handles "[sort]::a.name.or.something.else" * * @param ctx - * @return a Term or an operator, depending on the referenced object. + * @return a JTerm or an operator, depending on the referenced object. */ @Override public Object visitFuncpred_name(JavaKeYParser.Funcpred_nameContext ctx) { @@ -1666,7 +1668,7 @@ public JTerm visitAccessterm(JavaKeYParser.AccesstermContext ctx) { for (QuantifiableVariable qv : args[i].freeVars()) { if (boundVars.contains(qv)) { semanticError(ctx, - "Building function term " + op + "Building function JTerm " + op + " with bound variables failed: " + "Variable " + qv + " must not occur free in subterm " + args[i]); } @@ -1674,7 +1676,7 @@ public JTerm visitAccessterm(JavaKeYParser.AccesstermContext ctx) { } } ImmutableArray finalBoundVars = boundVars; - // create term + // create JTerm JTerm[] finalArgs1 = args; current = capsulateTf(ctx, () -> getTermFactory().createTerm(finalOp, finalArgs1, finalBoundVars, null)); @@ -1773,7 +1775,7 @@ private JTerm toNum(String number) { } /* - * private Term makeBinaryTerm(String opName, Term a, Term a1) { LDT ldt = + * private JTerm makeBinaryTerm(String opName, JTerm a, JTerm a1) { LDT ldt = * services.getTypeConverter().getLDTFor(a.sort()); if (ldt != null) { Function op = * ldt.getFunctionFor(opName, services); if (op == null) { * semanticError("Cannot resolve symbol '" + opName + "' for sort " + a.sort()); } else { a = @@ -1856,15 +1858,19 @@ private boolean isPackage(String name) { } } - protected boolean isHeapTerm(JTerm term) { - return term != null - && term.sort() == getServices().getTypeConverter().getHeapLDT().targetSort(); + protected boolean isHeapTerm(JTerm JTerm) { + return JTerm != null + && JTerm.sort() == getServices().getTypeConverter().getHeapLDT().targetSort(); } private boolean isSequenceTerm(JTerm reference) { return reference != null && reference.sort().name().equals(SeqLDT.NAME); } + private boolean inMultisetTerm(JTerm reference) { + return reference != null && reference.sort().name().equals(MSetLDT.NAME); + } + private boolean isIntTerm(JTerm reference) { return reference.sort().name().equals(IntegerLDT.NAME); } @@ -1888,54 +1894,54 @@ private boolean isImplicitHeap(JTerm t) { * Guard for {@link #replaceHeap0(JTerm, JTerm, ParserRuleContext)} to protect the double * application of {@code @heap}. */ - private JTerm replaceHeap(JTerm term, JTerm heap, ParserRuleContext ctx) { - if (explicitHeap.contains(term)) { - return term; + private JTerm replaceHeap(JTerm JTerm, JTerm heap, ParserRuleContext ctx) { + if (explicitHeap.contains(JTerm)) { + return JTerm; } - JTerm t = replaceHeap0(term, heap, ctx); + JTerm t = replaceHeap0(JTerm, heap, ctx); markHeapAsExplicit(t); return t; } - private JTerm replaceHeap0(JTerm term, JTerm heap, ParserRuleContext ctx) { - if (isSelectTerm(term)) { - if (!isImplicitHeap(term.sub(0))) { + private JTerm replaceHeap0(JTerm JTerm, JTerm heap, ParserRuleContext ctx) { + if (isSelectTerm(JTerm)) { + if (!isImplicitHeap(JTerm.sub(0))) { // semanticError(null, "Expecting program variable heap as first argument of: %s", - // term); - return term; + // JTerm); + return JTerm; } - JTerm[] params = { heap, replaceHeap(term.sub(1), heap, ctx), term.sub(2) }; + JTerm[] params = { heap, replaceHeap(JTerm.sub(1), heap, ctx), JTerm.sub(2) }; return capsulateTf(ctx, - () -> getServices().getTermFactory().createTerm(term.op(), params)); - } else if (term.op() instanceof ObserverFunction) { - if (!isImplicitHeap(term.sub(0))) { + () -> getServices().getTermFactory().createTerm(JTerm.op(), params)); + } else if (JTerm.op() instanceof ObserverFunction) { + if (!isImplicitHeap(JTerm.sub(0))) { semanticError(null, "Expecting program variable heap as first argument of: %s", - term); + JTerm); } - JTerm[] params = new JTerm[term.arity()]; + JTerm[] params = new JTerm[JTerm.arity()]; params[0] = heap; - params[1] = replaceHeap(term.sub(1), heap, ctx); + params[1] = replaceHeap(JTerm.sub(1), heap, ctx); for (int i = 2; i < params.length; i++) { - params[i] = term.sub(i); + params[i] = JTerm.sub(i); } return capsulateTf(ctx, - () -> getServices().getTermFactory().createTerm(term.op(), params)); + () -> getServices().getTermFactory().createTerm(JTerm.op(), params)); } - return term; + return JTerm; } /** * Replace standard heap by another heap in an observer function. */ - protected JTerm heapSelectionSuffix(JTerm term, JTerm heap, ParserRuleContext ctx) { + protected JTerm heapSelectionSuffix(JTerm JTerm, JTerm heap, ParserRuleContext ctx) { if (!isHeapTerm(heap)) { - semanticError(null, "Expecting term of type Heap but sort is %s for term %s", - heap.sort(), term); + semanticError(null, "Expecting JTerm of type Heap but sort is %s for JTerm %s", + heap.sort(), JTerm); } - JTerm result = replaceHeap(term, heap, ctx); + JTerm result = replaceHeap(JTerm, heap, ctx); return result; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index 78818a43e31..74985d1ee89 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java @@ -7,6 +7,9 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Statement; +import de.uka.ilkd.key.java.ast.StatementBlock; +import de.uka.ilkd.key.java.ast.StatementContainer; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.abstraction.Type; import de.uka.ilkd.key.java.ast.ccatch.*; @@ -16,6 +19,7 @@ import de.uka.ilkd.key.java.ast.expression.literal.*; import de.uka.ilkd.key.java.ast.expression.operator.*; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.*; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.java.visitor.Visitor; @@ -406,6 +410,55 @@ public void performActionOnSeqPut(SeqPut x) { printDLFunctionOperator("\\seq_upd", x); } + @Override + public void performActionOnEmptyMSetLiteral(EmptyMSetLiteral x) { + layouter.print("\\mset_empty"); + } + + + + @Override + public void performActionOnMSetUnion(MSetUnion x) { + printDLFunctionOperator("\\mset_union", x); + } + + @Override + public void performActionOnMSetIntersect( + MSetIntersect x) { + printDLFunctionOperator("\\mset_intersection", x); + } + + @Override + public void performActionOnMSetSum(MSetSum x) { + printDLFunctionOperator("\\mset_sum", x); + } + + @Override + public void performActionOnMSetDiff(MSetDiff x) { + printDLFunctionOperator("\\mset_diff", x); + } + + @Override + public void performActionOnMSetSingle( + MSetSingle x) { + printDLFunctionOperator("\\mset_single", x); + } + + @Override + public void performActionOnMSetMul(MSetMul x) { + x.getChildAt(0).visit(this); + layouter.print("["); + x.getChildAt(1).visit(this); + layouter.print("]"); + } + + @Override + public void performActionOnMSetCard(MSetCard x) { + x.getChildAt(0).visit(this); + layouter.print(".length"); + } + + @Override public void performActionOnDLEmbeddedExpression(DLEmbeddedExpression x) { layouter.print("\\dl_" + x.getFunctionSymbol().name()); @@ -623,8 +676,10 @@ public void performActionOnTypeReference(TypeReference x, boolean fullTypeNames) } } - private void printTypeReference(ReferencePrefix prefix, @Nullable KeYJavaType type, - ProgramElementName name, boolean fullTypeNames) { + private void printTypeReference(ReferencePrefix prefix, + @Nullable KeYJavaType type, + ProgramElementName name, + boolean fullTypeNames) { printReferencePrefix(prefix); if (fullTypeNames && type != null) { layouter.print(type.getFullName()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java index 390324347d4..9a8b11c2696 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java @@ -396,6 +396,33 @@ public JTerm upperBound(JTerm a, LogicVariable lv) { return buildBigintTruncationExpression(resultType, t); } + private @NonNull SLExpression nonNumeralQuantifier(KeYJavaType declsType, boolean nullable, + Iterable qvs, JTerm t1, JTerm t2, @Nullable KeYJavaType resultType, + UnboundedNumericalQuantifier unbounded, BoundedNumericalQuantifier bounded) { + Iterator it = qvs.iterator(); + LogicVariable lv = it.next(); + JTerm t; + if (it.hasNext() || !isBoundedNumerical(t1, lv)) { + // not interval range, create unbounded comprehension term + ImmutableList _qvs = + ImmutableList.of().prepend(lv); + while (it.hasNext()) { + _qvs = _qvs.prepend(it.next()); + } + t = unbounded.apply(declsType, nullable, _qvs, t1, t2); + } else { + t = bounded.apply(lv, lowerBound(t1, lv), upperBound(t1, lv), t2); + } + + if (resultType == null) { + resultType = services.getTypeConverter().getKeYJavaType(t2); + } + + // cast to specific JML type (fixes bug #1347) + return new SLExpression(t, resultType); + } + + public ImmutableList infflowspeclist(ImmutableList result) { return result; } @@ -879,6 +906,22 @@ public SLExpression createSeqDef(SLExpression a, SLExpression b, SLExpression t, return new SLExpression(resultTerm, seqtype); } + public SLExpression createMsetRange(SLExpression left, SLExpression right, SLExpression supplier, + KeYJavaType declsType, ImmutableList declVars) { + if (!(declsType.getJavaType().equals(PrimitiveType.JAVA_INT) + || declsType.getJavaType().equals(PrimitiveType.JAVA_BIGINT))) { + throw exc.createException0( + "msetRange definition variable must be of type int or \\bigint"); + } else if (declVars.size() != 1) { + throw exc.createException0("msetRange definition must declare exactly one variable"); + } + QuantifiableVariable qv = declVars.head(); + JTerm supplierTerm = ensureTerm(supplier.getTerm()); + JTerm resultTerm = tb.msetRange(qv, left.getTerm(), right.getTerm(), supplierTerm, supplierTerm.sort()); + final KeYJavaType msetType = services.getJavaInfo().getPrimitiveKeYJavaType("\\mSet"); + return new SLExpression(resultTerm, msetType); + } + public SLExpression createUnionF(boolean nullable, Pair> declVars, JTerm expr, JTerm guard) { final JavaInfo javaInfo = services.getJavaInfo(); @@ -1213,7 +1256,6 @@ public SLExpression skolemExprHelper(String jmlKeyWord, KeYJavaType type, return skolemExprHelper(type, services, jmlKeyWord); } - public @NonNull SLExpression skolemExprHelper(@NonNull KeYJavaType type, @NonNull TermServices services, @NonNull String shortName) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index 9d71c0b7b94..357acf2a256 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java @@ -1743,8 +1743,10 @@ public SLExpression visitSpecquantifiedexpression( expr.getType()); case JmlLexer.MAX -> termFactory.quantifiedMax(guard, body, declVars.first, nullable, declVars.second); + case JmlLexer.MIN -> termFactory.quantifiedMin(guard, body, declVars.first, nullable, declVars.second); + case JmlLexer.NUM_OF -> { KeYJavaType kjtInt = services.getTypeConverter().getKeYJavaType(PrimitiveType.JAVA_BIGINT); @@ -1861,6 +1863,21 @@ public Object visitSeqdefterm(JmlParser.SeqdeftermContext ctx) { return result; } + @Override + public Object visitMsetrangeterm(JmlParser.MsetrangetermContext ctx) { + Pair> decls = accept(ctx.quantifiedvardecls()); + resolverManager.pushLocalVariablesNamespace(); + assert decls != null; + resolverManager.putIntoTopLocalVariablesNamespace(decls.second, decls.first); + SLExpression left = accept(ctx.expression(0)); + SLExpression right = accept(ctx.expression(1)); + SLExpression supplier = accept(ctx.expression(2)); + assert supplier != null; + SLExpression result = termFactory.createMsetRange(left, right, supplier, decls.first, decls.second); + resolverManager.popLocalVariablesNamespace(); + return result; + } + @Override public Pair> visitQuantifiedvardecls( JmlParser.QuantifiedvardeclsContext ctx) { diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key index 381662fdc6a..99253bf46b0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key @@ -31,4 +31,5 @@ freeADT, wellfound, "./string/charListHeader.key", - types; + types, + "./mset/msetHeader.key"; diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetAxioms.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetAxioms.key new file mode 100644 index 00000000000..62aaf9ce9b5 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetAxioms.key @@ -0,0 +1,296 @@ + +\rules{ + + defOfMSetEmpty{ + \schemaVar \term any msetEl; + \schemaVar \variables int x; + + \find(msetEmpty) + + \varcond(\notFreeIn(x, msetEl)) + \replacewith(mset{x;}(0, 0, msetEl)) + }; + + defOfMSetSingle{ + \schemaVar \term any msetEl; + \schemaVar \variables int x; + + \find(msetSingle(msetEl)) + + \varcond(\notFreeIn(x, msetEl)) + \replacewith(mset{x;}(0, 1, msetEl)) + }; + + defOfMSetSum{ + \schemaVar \term Mset m, s; + \schemaVar \term any msetEl; + \schemaVar \variables int x; + + \find(msetIntersec(m, s)) + \varcond(\notFree(x, m), + \notFree(x, s), + \notFree(x, msetEl)) + + \replacewith( mset(m) + mset(s)) + }; + \lemma + msetSumWithMSetEmpty1{ + + \find(msetSum(msetEmpty, msetEmpty)) + \replacewith(msetEmpty) + + \heuristics(concrete) + \displayname "msetSumWithEmpty" + }; + + \lemma + msetSumWithMSetEmpty2{ + \schemaVar \term Mset m; + + \find(msetSum(m, msetEmpty)) + \replacewith(m) + + \heuristics(concrete) + \displayname "msetSumWithEmpty" + }; + + \lemma + msetSumWithMSetEmpty3{ + \schemaVar \term any msetEl; + + \find(msetSum(msetSingle(msetEl), msetEmpty)) + \replacewith(msetSingle(msetEl)) + + \heuristics(concrete) + \displayname "msetSumWithEmpty" + }; + + \lemma + msetSumWithMSetSingle1{ + \schemaVar \term any msetEl; + + \find(msetSum(msetSingle(msetEl), msetSingle(msetEl))) + \replacewith(msetSingle(msetEl) + msetSingle(msetEL)) + \heuristics(concrete) + \displayname "msetSumWithSingle" + + }; + + \lemma + \msetSumWithMSetSingle2{ + \schemaVar \term Mset m; + \schemaVar \term any msetEl; + + \find(msetSum(m, msetSingle(msetEl))) + \replacewith(m + msetSingle(msetEl)) + \heuristics(concrete) + \displayname "msetSumWithSingle" + + }; + + + \lemma + msetSumCommutativity { + \schemaVar \term Mset m, s; + \find(msetSum(m, s)) + \replacewith(msetSum(s, m)) + \heuristics(concrete) + }; + + \lemma + msetSumAssociativity { + \schemaVar \term Mset m, s, t; + \find(msetSum(m, msetSum(s, t))) + \replacewith(msetSum(msetSum(m, s), t)) + }; + + + \lemma + msetSummWithSameMSets{ + \schemaVar \term Mset m; + \find(msetSum(m,m)) + \replace(m * 2) + \heuristics(concrete) + + }; + + \lemma + msetDiffWithMSetEmpty1{ + + \find(msetDiff(msetEmpty, msetEmpty)) + \replacewith(msetEmpty) + + \heuristics(concrete) + \displayname "msetDiffWithEmpty" + }; + + \lemma + msetDiffWithMSetEmpty2{ + \schemaVar \term Mset m; + + \find(msetDiff(m, msetEmpty)) + \replacewith(m) + + \heuristics(concrete) + \displayname "msetDiffWithEmpty" + }; + + \lemma + msetDiffWithMSetEmpty3{ + \schemaVar \term any msetEl; + + \find(msetDiff(msetSingle(msetEl), msetEmpty)) + \replacewith(msetSingle(msetEl)) + + \heuristics(concrete) + \displayname "msetDiffWithEmpty" + }; + + + + \lemma + \msetDiffWithMSetSingle1{ + \schemaVar \term any msetEl; + + \find(msetDiff(msetSingle(msetEl), msetSingle(msetEl))) + \replacewith(msetEmpty) + \heuristics(concrete) + \displayname "msetDiffWithSingle" + + }; + + \lemma + \msetDiffWithMSetSingle2{ + \schemaVar \term any msetEl1, msetEl2; + + \find(msetDiff(msetSingle(msetEl1), msetSingle(msetEl2))) + \replace(msetSum(msetSingle(msetEl1), msetSingle(msetEl2))) + + \heuristics(concrete) + \displayname "msetDiffWithSingle" + + }; + + \lemma + msetDiffWithMSetSingle3{ + \schemaVar \term Mset m; + \schemaVar \term any msetEl; + + \find(msetDiff(m, msetSingle(msetEl))) + \replacewith(\if(msetMul(m, msetEl) > 0 && msetMul(msetSingle(msetEl), msetEl) == 1) + \than(m) + \else(msetSum(m, msetSingle(msetEl)))) + + \heuristics(concrete) + \displayname "msetDiffWithSingle" + + }; + + \lemma + msetDiffCommutativity{ + \schemaVar \term Mset m, s; + \find(msetDiff(m, s)) + \replacewith(msetDiff(s, m)) + \heuristics(concrete) + + }; + + +mset_split { + \schemaVar \term int low, high; + \schemaVar \term int middle; + \variables int uSub, uSub1, uSub2; + + + \find(mset{uSub;}(low, high, t)) + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, middle), + \notFreeIn(uSub, high)) + \replacewith(\if(low <= middle & middle <= high) + \then(msetSum(mset{uSub;}(low, middle, t), mset{uSub;}(middle, high, t))) + \else(mset{uSub;}(low, high, t))) + + \heuristics(comprehension_split, triggered) + + \trigger {middle} mset{uSub;}(low, middle, t) \avoid middle <= low, middle >= high; + }; + +} + + + + mset_Single{ + \schemaVar \term int low, high; + \schemaVar \term any t; + \schemaVar \variables int uSub; + + \find(mset{uSub;}(low, high, t)) + + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, high)) + + \replacewith(\if(high - low = 1) + \then(msetSingle(t)) + \else(mset{uSub;}(low, high, t))) + + } + + +mset_extract_triggered_back_2 { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(tempMset{uSub;}(low, high, beta :: select(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, high), + \notFreeIn(uSub, h), + \notFreeIn(uSub, array)) + \replacewith( + \if(low = high) + \then(msetSingle(beta :: select(h, array, arr(high)))) + \else(msetSum(tempMset{uSub;}(low, high - 1, beta :: select(h, array, arr(uSub))), + msetSingle(beta :: select(h, array, arr(high))))) + ) + \heuristics(simplify_ENLARGING) +}; + + + mset_extract_triggered_front { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(tempMset{uSub;}(low, high, beta::select(h,array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, high), + \notFreeIn(uSub, h), + \notFreeIn(uSub, array)) + \replacewith(msetSum(msetSingle(beta::select(h,array, arr(low))), + tempMset{uSub;}(low+1, high, beta :: select(h, array, arr(uSub))))) + + \heuristics(comprehension_split, triggered) + \trigger {low} msetSingle(beta::select(h,array, arr(low))) + \avoid low >= high, false; + }; + + mset_extract_triggered_back { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(tempMset{uSub;}(low, high, beta::select(h,array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, high), + \notFreeIn(uSub, h), + \notFreeIn(uSub, array)) + \replacewith(msetSum(msetSingle(beta::select(h,array, arr(high))), + tempMset{uSub;}(low, high-1, beta :: select(h, array, arr(uSub))))) + + \heuristics(comprehension_split, triggered) + \trigger {high} msetSingle(beta::select(h,array, arr(high))) + \avoid high <= low, false; + }; diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetHeader.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetHeader.key new file mode 100644 index 00000000000..e3c3003b4bd --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetHeader.key @@ -0,0 +1,18 @@ +\sorts { + \generic El; + \generic SubEl \extends El; + Mset<[El]>; +} + +\functions { + // Getters + int msetMul(Mset<[El]>, El); + int msetCard(Mset<[El]>); + + // Constructors + Mset<[El]> msetEmpty<[El]>; + Mset<[El]> msetSingle<[El]>(El); + Mset<[El]> msetDiff<[El]>(Mset<[El]>, Mset<[El]>); + Mset<[El]> msetSum<[El]>(Mset<[El]>, Mset<[El]>); + Mset<[El]> msetRange<[El]> {false, false, true}(int, int, El); +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetRules.key new file mode 100644 index 00000000000..4bb9ea9f684 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetRules.key @@ -0,0 +1,210 @@ + +\rules { + + mset_Empty { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term SubEl t; + + \find(msetRange<[El]>{uSub;}(left, right, t)) + \varcond(\notFreeIn(uSub, left)) + \replacewith(\if(right < left) + \then(msetEmpty<[El]>) + \else(msetRange<[El]>{uSub;}(left, right, t))) + + \heuristics(simplify) + }; + + mset_Single { + \schemaVar \term int left; + \schemaVar \variables int uSub; + \schemaVar \term SubEl t; + + \find(msetRange<[El]>{uSub;}(left, left, t)) + \sameUpdateLevel + \replacewith(msetSingle({\subst uSub; left}(t))) + \heuristics(simplify) + }; + + msetSumWithMsetEmpty1 { + \schemaVar \term Mset m; + \find(msetSum<[El]>(msetEmpty<[El]>, m)) + \replacewith(m) + \heuristics(simplify) + \displayname "msetSumWithEmpty" + }; + + msetSumWithmsetEmpty2 { + \schemaVar \term Mset m; + \find(msetSum<[El]>(m, msetEmpty<[El]>)) + \replacewith(m) + \heuristics(simplify) + \displayname "msetSumWithEmpty" + }; + + msetSumCommutativity { + \schemaVar \term Mset commLeft, commRight; + \find(msetSum<[El]>(commLeft, commRight)) + \replacewith(msetSum<[El]>(commRight, commLeft)) + \heuristics(polySimp_expand, polySimp_addOrder) + }; + + msetSumAssociativity { + \schemaVar \term Mset addAssocPoly0, addAssocPoly1, addAssocMono; + \find(msetSum<[El]>(addAssocPoly0, msetSum<[El]>(addAssocPoly1, addAssocMono))) + \replacewith(msetSum<[El]>(msetSum<[El]>(addAssocPoly0, addAssocPoly1), addAssocMono)) + \heuristics(polySimp_expand, polySimp_addAssoc) + }; + + msetDiffWithMsetEmpty1 { + \find(msetDiff<[El]>(msetEmpty<[El]>, msetEmpty<[El]>)) + \replacewith(msetEmpty<[El]>) + \heuristics(simplify) + \displayname "msetDiffWithEmpty" + }; + + msetDiffWithMsetEmpty2 { + \schemaVar \term Mset m; + \find(msetDiff<[El]>(m, msetEmpty<[El]>)) + \replacewith(m) + \heuristics(simplify) + \displayname "msetDiffWithEmpty" + }; + + msetDiffCommutativity { + \schemaVar \term Mset commLeft, commRight; + \find(msetDiff<[El]>(commLeft, commRight)) + \replacewith(msetDiff<[El]>(commRight, commLeft)) + \heuristics(order_terms) + }; + + mset_split { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \variables int uSub; + \schemaVar \term SubEl t; + + \find(msetRange<[El]>{uSub;}(left, right, t)) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum<[El]>( + msetRange<[El]>{uSub;}(left, middle-1, t), + msetRange<[El]>{uSub;}(middle, right, t))) + \else(msetRange<[El]>{uSub;}(left, right, t))) + }; + + mset_extract_triggered { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left, middle, right, h, array)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum<[El]>(msetSum<[El]>(msetRange<[El]>{uSub;}(left, middle-1, select<[SubEl]>(h, array, arr(uSub))), + msetSingle<[El]>(select<[SubEl]>(h, array, arr(middle)))), + msetRange<[El]>{uSub;}(middle+1, right, select<[SubEl]>(h, array, arr(uSub))))) + \else(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(comprehension_split, triggered) + \trigger {middle} msetSingle<[El]>(select<[SubEl]>(h, array, arr(middle))) + \avoid middle <= -1 + left, right <= -1 + middle; + }; + + // that rule seems not to be correct middle -1 can be < left, how is range for an empty negative interval defined? + mset_extract_array { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \variables int uSub; + \schemaVar \term SubEl x; + + \find(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(store(h, array, arr(middle), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum<[El]>(msetSum<[El]>(msetRange<[El]>{uSub;}(left, middle-1, select<[SubEl]>(h, array, arr(uSub))), + msetSingle<[El]>({\subst uSub; middle} x)), + msetRange<[El]>{uSub;}(middle+1, right, select<[SubEl]>(h, array, arr(uSub))))) + \else(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(simplify_ENLARGING) + }; + + mset_extract_array { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \variables int uSub; + \schemaVar \term SubEl x; + + \find(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(store(h, array, arr(middle), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum<[El]>(msetSum<[El]>(msetRange<[El]>{uSub;}(left, middle-1, select<[SubEl]>(h, array, arr(uSub))), + msetSingle<[El]>({\subst uSub; middle} x)), + msetRange<[El]>{uSub;}(middle+1, right, select<[SubEl]>(h, array, arr(uSub))))) + \else(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(simplify_ENLARGING) + }; + + mset_extract_array_front { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \term SubEl x; + + \find(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(store(h, array, arr(left), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right)) + \replacewith(msetSum<[El]>(msetSingle<[El]>({\subst uSub; left} x), + msetRange<[El]>{uSub;}(left+1, right, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(simplify_enlarging) + }; + + mset_extract_array_back { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \term SubEl x; + + \find(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(store(h, array, arr(right), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right)) + \replacewith(msetSum<[El]>(msetRange<[El]>{uSub;}(left, right-1, + select<[SubEl]>(h, array, arr(uSub))), + msetSingle<[El]>({\subst uSub; right} x))) + \heuristics(simplify_enlarging) + }; + + mset_extract_triggered_front { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange<[El]>{uSub;}(low, high, select<[SubEl]>(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) + \replacewith(msetSum<[El]>(msetSingle<[El]>(select<[SubEl]>(h, array, arr(low))), + msetRange<[El]>{uSub;}(low+1, high, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(comprehension_split, triggered) + \trigger {low} msetSingle<[El]>(select<[SubEl]>(h, array, arr(low))) + \avoid low >= high, false; + }; + + mset_extract_triggered_back { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange<[El]>{uSub;}(low, high, select<[SubEl]>(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) + \replacewith(msetSum<[El]>(msetSingle<[El]>(select<[SubEl]>(h, array, arr(high))), + msetRange<[El]>{uSub;}(low, high-1, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(comprehension_split, triggered) + \trigger {high} msetSingle<[El]>(select<[SubEl]>(h, array, arr(high))) + \avoid high <= low, false; + }; +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key index ebbbb59ad82..4a5b0d307c0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key @@ -48,6 +48,7 @@ \include "./sequence/seqPerm.key"; \include "./sequence/seqPerm2.key"; \include "./set/setRules.key"; +\include "./mset/msetRules.key"; // rules for Java (order does not matter, since not provable anyway) \include javaRules; diff --git a/key.ui/examples/heap/quicksort_mset/Quicksort.java b/key.ui/examples/heap/quicksort_mset/Quicksort.java new file mode 100644 index 00000000000..a4c013082ac --- /dev/null +++ b/key.ui/examples/heap/quicksort_mset/Quicksort.java @@ -0,0 +1,77 @@ +/** + * This shows how MultiSets can be used to verify the permutation property + * of a sorting algorithm. + * FIXME: The sortedness property is NOT shown. + * The source code is the same as quicksort/QuickSort.java but the present + * specification is proven automatically, without proof scripts. + * + * @author Silvia Zoraqi, Lukas Grätz, 2025 + * + * based on: + * @author Mattias Ulbrich, 2015 + */ + +class Quicksort { + + /*@ public normal_behaviour + @ ensures (\mset int k; 0 <= k < array.length; array[k]) == \old((\mset int k; 0 <= k < array.length; array[k])); + @ assignable array[*]; + @*/ + public void sort(int[] array) { + if(array.length > 0) { + sort(array, 0, array.length-1); + } + } + + /*@ public normal_behaviour + @ requires 0 <= from; + @ requires to < array.length; + @ ensures (\mset int k; 0 <= k < array.length; array[k]) == \old((\mset int k; 0 <= k < array.length; array[k])); + @ assignable array[*]; + @ measured_by to - from + 1; + @*/ + private void sort(int[] array, int from, int to) { + if(from < to) { + int splitPoint = split(array, from, to); + sort(array, from, splitPoint-1); + sort(array, splitPoint+1, to); + } + } + + /*@ public normal_behaviour + @ requires 0 <= from && from < to && to <= array.length-1; + @ ensures (\mset int k; 0 <= k < array.length; array[k]) == \old((\mset int k; 0 <= k < array.length; array[k])); + @ ensures from <= \result && \result <= to; + @ assignable array[*]; + @*/ + private int split(int[] array, int from, int to) { + + int i = from; + int pivot = array[to]; + + /*@ + @ loop_invariant from <= i && i <= j; + @ loop_invariant from <= j && j <= to; + @ loop_invariant (\mset int k; 0 <= k < array.length; array[k]) == \old((\mset int k; 0 <= k < array.length; array[k])); + @ decreases to + to - j - i + 2; + @ assignable array[*]; + @*/ + for(int j = from; j < to; j++) { + if(array[j] <= pivot) { + int t = array[i]; + array[i] = array[j]; + array[j] = t; + i++; + } + } + + // FIXME: this assignment has no effect, it should be a loop invariant + pivot = array[to]; + + array[to] = array[i]; + array[i] = pivot; + + return i; + + } +}