From d026c5cbe9389cd551b54443c05d5c0a85d7c1e7 Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Tue, 28 Nov 2023 17:33:40 +0100 Subject: [PATCH 01/42] Hopefully (yet untested) fixed previous 'assigns' and also introduced 'loop_modifies' and 'loop_writes' from OpenJML as JML aliases --- key.core/src/main/antlr4/JmlLexer.g4 | 7 +++---- key.core/src/main/antlr4/JmlParser.g4 | 4 +++- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index f1a67a2afd5..bfb5ef93228 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -74,8 +74,8 @@ fragment Pfree: '_free'?; //suffix ACCESSIBLE: 'accessible' Pred -> pushMode(expr); ASSERT: 'assert' Pred -> pushMode(expr); ASSUME: 'assume' Pred -> pushMode(expr); -ASSIGNABLE: 'assignable' Pfree -> pushMode(expr); -ASSIGNS: 'assigns' Pred -> pushMode(expr); +ASSIGNABLE: ('assignable' | 'assigns' | 'assigning') Pfree -> pushMode(expr); +LOOP_ASSIGNABLE: ('loop_modifies' | 'loop_writes') (Pfree|Pred) -> pushMode(expr); AXIOM: 'axiom' -> pushMode(expr); BREAKS: 'breaks' -> pushMode(expr); CAPTURES: 'captures' Pred -> pushMode(expr); @@ -105,8 +105,7 @@ MEASURED_BY: 'measured_by' Pred -> pushMode(expr); MERGE_POINT: 'merge_point'; MERGE_PROC: 'merge_proc'; MERGE_PARAMS: 'merge_params' -> pushMode(expr); -MODIFIABLE: 'modifiable' Pred -> pushMode(expr); -MODIFIES: 'modifies' Pred -> pushMode(expr); +MODIFIABLE: ('modifiable' | 'modifies') Pred -> pushMode(expr); MONITORED: 'monitored' -> pushMode(expr); MONITORS_FOR: 'monitors_for' -> pushMode(expr); //OLD: 'old' -> pushMode(expr); diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index a66965df0fd..1de7aba7f3f 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -87,7 +87,7 @@ accessible_clause (lhs=expression COLON)? rhs=storeRefUnion (MEASURED_BY mby=expression)? SEMI_TOPLEVEL; -assignable_clause: (ASSIGNABLE|MODIFIES|MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; +assignable_clause: (ASSIGNABLE | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; //depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ; //decreases_clause: DECREASES termexpression (COMMA termexpression)*; represents_clause @@ -175,9 +175,11 @@ loop_specification | loop_separates_clause | loop_determines_clause | assignable_clause + | loop_assignable_clause | variant_function)*; loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL; +loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL; //loop_separates_clause: SEPARATES expression; //loop_determines_clause: DETERMINES expression; From b35e0a895adf6e6211659ca74913441993b40748 Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Tue, 28 Nov 2023 18:09:33 +0100 Subject: [PATCH 02/42] Re-added MODIFIES as it was also used somewhere else --- key.core/src/main/antlr4/JmlLexer.g4 | 3 ++- key.core/src/main/antlr4/JmlParser.g4 | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index bfb5ef93228..75bb8d4b1f3 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -105,7 +105,8 @@ MEASURED_BY: 'measured_by' Pred -> pushMode(expr); MERGE_POINT: 'merge_point'; MERGE_PROC: 'merge_proc'; MERGE_PARAMS: 'merge_params' -> pushMode(expr); -MODIFIABLE: ('modifiable' | 'modifies') Pred -> pushMode(expr); +MODIFIABLE: 'modifiable' Pred -> pushMode(expr); +MODIFIES: 'modifies' Pred -> pushMode(expr); MONITORED: 'monitored' -> pushMode(expr); MONITORS_FOR: 'monitors_for' -> pushMode(expr); //OLD: 'old' -> pushMode(expr); diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index 1de7aba7f3f..23c20a54994 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -87,7 +87,7 @@ accessible_clause (lhs=expression COLON)? rhs=storeRefUnion (MEASURED_BY mby=expression)? SEMI_TOPLEVEL; -assignable_clause: (ASSIGNABLE | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; +assignable_clause: (ASSIGNABLE | MODIFIES | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; //depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ; //decreases_clause: DECREASES termexpression (COMMA termexpression)*; represents_clause @@ -179,7 +179,7 @@ loop_specification | variant_function)*; loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL; -loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; +loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE | MODIFIES | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL; //loop_separates_clause: SEPARATES expression; //loop_determines_clause: DETERMINES expression; From e65a8e8253df0ec91efce38c097e5a868b995b36 Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Wed, 29 Nov 2023 01:05:50 +0100 Subject: [PATCH 03/42] Added syntax highlighting --- .../java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java index 2eb275be4c5..cea30168b0f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java @@ -177,7 +177,10 @@ private enum CommentState { "\\working_space", "\\values", "\\inv", // clause keywords: "accessible", "accessible_redundantly", "assert", "assert_redundantly", "assignable", - "assignable_free", "assignable_redundantly", "assume", "assume_redudantly", "breaks", + "assignable_free", "assignable_redundantly", "assigns", "assigns_free", + "assigns_redundantly", "assigning", "assigning_free", "assigning_redundantly", + "loop_modifies", "loop_modifies_free", "loop_modifies_redundantly", "loop_writes", + "loop_writes_free", "loop_writes_redundantly"," assume", "assume_redudantly", "breaks", "breaks_redundantly", "\\by", "callable", "callable_redundantly", "captures", "captures_redundantly", "continues", "continues_redundantly", "debug", "\\declassifies", "decreases", "decreases_redundantly", "decreasing", "decreasing_redundantly", "diverges", From bfc513ce83ac1576c88f0d28a0807f260e37145f Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Wed, 29 Nov 2023 01:23:23 +0100 Subject: [PATCH 04/42] Removed one ambiguity --- key.core/src/main/antlr4/JmlParser.g4 | 1 - 1 file changed, 1 deletion(-) diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index 23c20a54994..96bc5ff50ac 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -174,7 +174,6 @@ loop_specification | determines_clause | loop_separates_clause | loop_determines_clause - | assignable_clause | loop_assignable_clause | variant_function)*; From 9b4e1fd40ac6ef3e1c38d0c119b17e6378bea5f3 Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Wed, 29 Nov 2023 01:31:24 +0100 Subject: [PATCH 05/42] Minor formatting --- .../main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java index cea30168b0f..6a71eebebf2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java @@ -180,7 +180,7 @@ private enum CommentState { "assignable_free", "assignable_redundantly", "assigns", "assigns_free", "assigns_redundantly", "assigning", "assigning_free", "assigning_redundantly", "loop_modifies", "loop_modifies_free", "loop_modifies_redundantly", "loop_writes", - "loop_writes_free", "loop_writes_redundantly"," assume", "assume_redudantly", "breaks", + "loop_writes_free", "loop_writes_redundantly", "assume", "assume_redudantly", "breaks", "breaks_redundantly", "\\by", "callable", "callable_redundantly", "captures", "captures_redundantly", "continues", "continues_redundantly", "debug", "\\declassifies", "decreases", "decreases_redundantly", "decreasing", "decreasing_redundantly", "diverges", From c9ed0b8d2b21580c0739d12f8d997c170547f6bd Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Wed, 29 Nov 2023 22:24:09 +0100 Subject: [PATCH 06/42] Mistakenly included redundancy suffix --- key.core/src/main/antlr4/JmlLexer.g4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index 75bb8d4b1f3..c4436657100 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -75,7 +75,7 @@ ACCESSIBLE: 'accessible' Pred -> pushMode(expr); ASSERT: 'assert' Pred -> pushMode(expr); ASSUME: 'assume' Pred -> pushMode(expr); ASSIGNABLE: ('assignable' | 'assigns' | 'assigning') Pfree -> pushMode(expr); -LOOP_ASSIGNABLE: ('loop_modifies' | 'loop_writes') (Pfree|Pred) -> pushMode(expr); +LOOP_ASSIGNABLE: ('loop_modifies' | 'loop_writes') Pfree -> pushMode(expr); AXIOM: 'axiom' -> pushMode(expr); BREAKS: 'breaks' -> pushMode(expr); CAPTURES: 'captures' Pred -> pushMode(expr); From 0ffead610249390fc980367e690a22d72f857f1d Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Wed, 21 Feb 2024 17:49:56 +0100 Subject: [PATCH 07/42] Integrated port of loop assignable at HackeYthon --- .../key/speclang/njml/TextualTranslator.java | 29 +++++++++++++++++-- .../ilkd/key/speclang/njml/Translator.java | 16 ++++++++++ 2 files changed, 43 insertions(+), 2 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java index 20ecef050c2..183e52dee3f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java @@ -12,6 +12,7 @@ import org.key_project.util.collection.ImmutableSLList; import org.antlr.v4.runtime.ParserRuleContext; +import org.antlr.v4.runtime.tree.TerminalNode; import org.antlr.v4.runtime.Token; import org.jspecify.annotations.Nullable; @@ -254,9 +255,10 @@ public Object visitAccessible_clause(JmlParser.Accessible_clauseContext ctx) { @Override public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) { Name[] heaps = visitTargetHeap(ctx.targetHeap()); + final TerminalNode assign = ctx.ASSIGNABLE() != null ? ctx.ASSIGNABLE() + : ctx.MODIFIES() != null ? ctx.MODIFIES() : ctx.MODIFIABLE(); final boolean isFree = - ctx.ASSIGNABLE() != null && ctx.ASSIGNABLE().getText().endsWith("_free") - || ctx.MODIFIES() != null && ctx.MODIFIES().getText().endsWith("_free"); + assign != null && assign.getText().endsWith("_free"); final LabeledParserRuleContext ctx2 = LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree ? OriginTermLabel.SpecType.ASSIGNABLE_FREE @@ -276,6 +278,29 @@ public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) { return null; } + @Override public Object visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) { + Name[] heaps = visitTargetHeap(ctx.targetHeap()); + final TerminalNode assign = ctx.ASSIGNABLE() != null ? ctx.ASSIGNABLE() + : ctx.MODIFIES() != null ? ctx.MODIFIES() : ctx.MODIFIABLE() != null ? + ctx.MODIFIABLE() : ctx.LOOP_ASSIGNABLE(); + final boolean isFree = + assign != null && assign.getText().endsWith("_free"); + final LabeledParserRuleContext ctx2 = + LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree + ? OriginTermLabel.SpecType.ASSIGNABLE_FREE + : OriginTermLabel.SpecType.ASSIGNABLE, + attachOriginLabel); + for (Name heap : heaps) { + if (loopContract != null) { + loopContract.addClause( + isFree ? TextualJMLLoopSpec.ClauseHd.ASSIGNABLE_FREE + : TextualJMLLoopSpec.ClauseHd.ASSIGNABLE, + heap, ctx2); + } + } + return null; + } + @Override public Object visitVariant_function(JmlParser.Variant_functionContext ctx) { final LabeledParserRuleContext ctx2 = 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 15de4187522..90c2c438552 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 @@ -2007,6 +2007,22 @@ public SLExpression visitAssignable_clause(JmlParser.Assignable_clauseContext ct return new SLExpression(t); } + @Override + public SLExpression visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) { + Term t; + LocationVariable[] heaps = visitTargetHeap(ctx.targetHeap()); + if (ctx.STRICTLY_NOTHING() != null) { + t = tb.strictlyNothing(); + } else { + final Term storeRef = accept(ctx.storeRefUnion()); + assert storeRef != null; + t = termFactory.assignable(storeRef); + } + for (LocationVariable heap : heaps) { + contractClauses.add(ContractClauses.ASSIGNABLE, heap, t); + } + return new SLExpression(t); + } @Override public SLExpression visitSignals_only_clause(JmlParser.Signals_only_clauseContext ctx) { From 097abe385cd906d538833ba9d777a8bd8a06f2d7 Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Wed, 21 Feb 2024 17:50:58 +0100 Subject: [PATCH 08/42] Applied spotless --- .../de/uka/ilkd/key/speclang/njml/TextualTranslator.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java index 183e52dee3f..a296f5d7ea7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java @@ -12,8 +12,8 @@ import org.key_project.util.collection.ImmutableSLList; import org.antlr.v4.runtime.ParserRuleContext; -import org.antlr.v4.runtime.tree.TerminalNode; import org.antlr.v4.runtime.Token; +import org.antlr.v4.runtime.tree.TerminalNode; import org.jspecify.annotations.Nullable; import static de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec.ClauseHd.INVARIANT; @@ -278,11 +278,12 @@ public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) { return null; } - @Override public Object visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) { + @Override + public Object visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) { Name[] heaps = visitTargetHeap(ctx.targetHeap()); final TerminalNode assign = ctx.ASSIGNABLE() != null ? ctx.ASSIGNABLE() - : ctx.MODIFIES() != null ? ctx.MODIFIES() : ctx.MODIFIABLE() != null ? - ctx.MODIFIABLE() : ctx.LOOP_ASSIGNABLE(); + : ctx.MODIFIES() != null ? ctx.MODIFIES() + : ctx.MODIFIABLE() != null ? ctx.MODIFIABLE() : ctx.LOOP_ASSIGNABLE(); final boolean isFree = assign != null && assign.getText().endsWith("_free"); final LabeledParserRuleContext ctx2 = From 394edd50012d432b8ad8b24c66c9e401ffed5089 Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Tue, 27 Feb 2024 18:41:00 +0100 Subject: [PATCH 09/42] Added more keywords (at least preliminarily and up for discussion) --- key.core/src/main/antlr4/JmlLexer.g4 | 9 ++++--- .../ilkd/key/gui/sourceview/JavaDocument.java | 24 ++++++++++++------- 2 files changed, 22 insertions(+), 11 deletions(-) diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index c4436657100..73d999b4242 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -75,7 +75,10 @@ ACCESSIBLE: 'accessible' Pred -> pushMode(expr); ASSERT: 'assert' Pred -> pushMode(expr); ASSUME: 'assume' Pred -> pushMode(expr); ASSIGNABLE: ('assignable' | 'assigns' | 'assigning') Pfree -> pushMode(expr); -LOOP_ASSIGNABLE: ('loop_modifies' | 'loop_writes') Pfree -> pushMode(expr); +LOOP_ASSIGNABLE + : ('loop_assignable' | 'loop_assigns' | 'loop_assigning' | + 'loop_modifiable' | 'loop_modifies' | 'loop_modifying' | + 'loop_writable' | 'loop_writes' | 'loop_writing') Pfree -> pushMode(expr); AXIOM: 'axiom' -> pushMode(expr); BREAKS: 'breaks' -> pushMode(expr); CAPTURES: 'captures' Pred -> pushMode(expr); @@ -105,8 +108,8 @@ MEASURED_BY: 'measured_by' Pred -> pushMode(expr); MERGE_POINT: 'merge_point'; MERGE_PROC: 'merge_proc'; MERGE_PARAMS: 'merge_params' -> pushMode(expr); -MODIFIABLE: 'modifiable' Pred -> pushMode(expr); -MODIFIES: 'modifies' Pred -> pushMode(expr); +MODIFIABLE: ('modifiable' | 'writable') Pred -> pushMode(expr); +MODIFIES: ('modifies' | 'modifying' | 'writes' | 'writing') Pred -> pushMode(expr); MONITORED: 'monitored' -> pushMode(expr); MONITORS_FOR: 'monitors_for' -> pushMode(expr); //OLD: 'old' -> pushMode(expr); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java index 6a71eebebf2..8eefe1e7c83 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java @@ -163,7 +163,7 @@ private enum CommentState { "spec_safe_math", "static", "strictfp", "strictly_pure", "synchronized", "transient", "two_state", "uninitialized", "volatile", - "no_state", "modifies", "erases", "modifiable", "returns", "break_behavior", + "no_state", "modifies", "modifying", "erases", "modifiable", "returns", "break_behavior", "continue_behavior", "return_behavior", // special JML expressions: "\\constraint_for", "\\created", "\\disjoint", "\\duration", "\\everything", "\\exception", @@ -176,14 +176,22 @@ private enum CommentState { "\\static_invariant_for", "\\strictly_nothing", "\\subset", "\\sum", "\\type", "\\typeof", "\\working_space", "\\values", "\\inv", // clause keywords: - "accessible", "accessible_redundantly", "assert", "assert_redundantly", "assignable", - "assignable_free", "assignable_redundantly", "assigns", "assigns_free", + "accessible", "accessible_redundantly", "assert", "assert_redundantly", + "assignable", "assignable_free", "assignable_redundantly", "assigns", "assigns_free", "assigns_redundantly", "assigning", "assigning_free", "assigning_redundantly", - "loop_modifies", "loop_modifies_free", "loop_modifies_redundantly", "loop_writes", - "loop_writes_free", "loop_writes_redundantly", "assume", "assume_redudantly", "breaks", - "breaks_redundantly", "\\by", "callable", "callable_redundantly", "captures", + "loop_assignable", "loop_assignable_free", "loop_assignable_redundantly", "loop_assigns", + "loop_assigns_free", "loop_assigns_redundantly", "loop_assigning", "loop_assigning_free", + "loop_assigning_redundantly", "loop_modifiable", "loop_modifiable_free", + "loop_modifiable_redundantly", "loop_modifies", "loop_modifies_free", + "loop_modifies_redundantly", "loop_modifying", "loop_modifying_free", + "loop_modifying_redundantly", "loop_writable", "loop_writable_free", + "loop_writable_redundantly", "loop_writes", "loop_writes_free", "loop_writes_redundantly", + "loop_writing", "loop_writing_free", "loop_writing_redundantly", + "assume", "assume_redudantly", "breaks", "breaks_redundantly", "\\by", + "callable", "callable_redundantly", "captures", "captures_redundantly", "continues", "continues_redundantly", "debug", "\\declassifies", - "decreases", "decreases_redundantly", "decreasing", "decreasing_redundantly", "diverges", + "decreases", "decreases_redundantly", "decreasing", "decreasing_redundantly", + "loop_variant", "loop_variant_redundantly", "diverges", "determines", "diverges_redundantly", "duration", "duration_redundantly", "ensures", "ensures_free", "ensures_redundantly", "\\erases", "forall", "for_example", "hence_by", "implies_that", "in", "in_redundantly", "\\into", "loop_invariant", "loop_invariant_free", @@ -195,7 +203,7 @@ private enum CommentState { "abrupt_behavior", "abrupt_behaviour", "also", "axiom", "behavior", "behaviour", "constraint", "exceptional_behavior", "exceptional_behaviour", "initially", "invariant", "invariant_free", "model_behavior", "model_behaviour", "monitors_for", "normal_behavior", - "normal_behaviour", "readable", "writable", + "normal_behaviour", "readable", "writable", "writes", "writing", // ADT functions: "\\seq_empty", "\\seq_def", "\\seq_singleton", "\\seq_get", "\\seq_put", "\\seq_reverse", "\\seq_length", "\\index_of", "\\seq_concat", "\\empty", "\\singleton", "\\set_union", From ece551beebd7af956003ea33725681b89ec171d5 Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Thu, 29 Feb 2024 16:24:35 +0100 Subject: [PATCH 10/42] Unify modifiable|modifying|modifies as the distinction has not been used anywhere --- key.core/src/main/antlr4/JmlLexer.g4 | 15 ++++++++------- key.core/src/main/antlr4/JmlParser.g4 | 4 ++-- .../ilkd/key/speclang/njml/TextualTranslator.java | 9 ++------- 3 files changed, 12 insertions(+), 16 deletions(-) diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index 73d999b4242..002c9d5896d 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -74,11 +74,14 @@ fragment Pfree: '_free'?; //suffix ACCESSIBLE: 'accessible' Pred -> pushMode(expr); ASSERT: 'assert' Pred -> pushMode(expr); ASSUME: 'assume' Pred -> pushMode(expr); -ASSIGNABLE: ('assignable' | 'assigns' | 'assigning') Pfree -> pushMode(expr); +ASSIGNABLE + : ('assignable' | 'assigns' | 'assigning' | + 'modifiable' | 'modifies' | 'modifying' | + 'writable' | 'writes' | 'writing') (Pfree|Pred) -> pushMode(expr); LOOP_ASSIGNABLE : ('loop_assignable' | 'loop_assigns' | 'loop_assigning' | 'loop_modifiable' | 'loop_modifies' | 'loop_modifying' | - 'loop_writable' | 'loop_writes' | 'loop_writing') Pfree -> pushMode(expr); + 'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred) -> pushMode(expr); AXIOM: 'axiom' -> pushMode(expr); BREAKS: 'breaks' -> pushMode(expr); CAPTURES: 'captures' Pred -> pushMode(expr); @@ -90,7 +93,7 @@ DECREASING: ('decreasing' | 'decreases' | 'loop_variant') Pred -> pushMode(expr) DETERMINES: 'determines' -> pushMode(expr); DIVERGES: 'diverges' Pred -> pushMode(expr); //DURATION: 'duration' Pred -> pushMode(expr); -ENSURES: ('ensures' (Pfree|Pred) | 'post' Pred )-> pushMode(expr); +ENSURES: ('ensures' | 'post') (Pfree|Pred) -> pushMode(expr); FOR_EXAMPLE: 'for_example' -> pushMode(expr); //FORALL: 'forall' -> pushMode(expr); //? HELPER: 'helper'; @@ -100,7 +103,7 @@ INITIALLY: 'initially' -> pushMode(expr); INSTANCE: 'instance'; INVARIANT: 'invariant' (Pfree|Pred) -> pushMode(expr); LOOP_CONTRACT: 'loop_contract'; -LOOP_INVARIANT: ('loop_invariant' (Pfree|Pred) | 'maintaining' Pred) -> pushMode(expr); +LOOP_INVARIANT: ('loop_invariant' | 'maintaining') (Pfree|Pred) -> pushMode(expr); LOOP_DETERMINES: 'loop_determines'; // internal translation for 'determines' in loop invariants LOOP_SEPARATES: 'loop_separates'; //KeY extension, deprecated MAPS: 'maps' Pred -> pushMode(expr); @@ -108,8 +111,6 @@ MEASURED_BY: 'measured_by' Pred -> pushMode(expr); MERGE_POINT: 'merge_point'; MERGE_PROC: 'merge_proc'; MERGE_PARAMS: 'merge_params' -> pushMode(expr); -MODIFIABLE: ('modifiable' | 'writable') Pred -> pushMode(expr); -MODIFIES: ('modifies' | 'modifying' | 'writes' | 'writing') Pred -> pushMode(expr); MONITORED: 'monitored' -> pushMode(expr); MONITORS_FOR: 'monitors_for' -> pushMode(expr); //OLD: 'old' -> pushMode(expr); @@ -117,7 +118,7 @@ MONITORS_FOR: 'monitors_for' -> pushMode(expr); //PRE: 'pre' Pred -> pushMode(expr); READABLE: 'readable'; REPRESENTS: 'represents' Pred -> pushMode(expr); -REQUIRES: ('requires' (Pfree|Pred) | 'pre' Pred) -> pushMode(expr); +REQUIRES: ('requires'| 'pre') (Pfree|Pred) -> pushMode(expr); RETURN: 'return' -> pushMode(expr); RETURNS: 'returns' -> pushMode(expr); RESPECTS: 'respects' -> pushMode(expr); diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index 96bc5ff50ac..804323c5cc5 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -87,7 +87,7 @@ accessible_clause (lhs=expression COLON)? rhs=storeRefUnion (MEASURED_BY mby=expression)? SEMI_TOPLEVEL; -assignable_clause: (ASSIGNABLE | MODIFIES | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; +assignable_clause: ASSIGNABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; //depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ; //decreases_clause: DECREASES termexpression (COMMA termexpression)*; represents_clause @@ -178,7 +178,7 @@ loop_specification | variant_function)*; loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL; -loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE | MODIFIES | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; +loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL; //loop_separates_clause: SEPARATES expression; //loop_determines_clause: DETERMINES expression; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java index a296f5d7ea7..975ede713e9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java @@ -255,10 +255,8 @@ public Object visitAccessible_clause(JmlParser.Accessible_clauseContext ctx) { @Override public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) { Name[] heaps = visitTargetHeap(ctx.targetHeap()); - final TerminalNode assign = ctx.ASSIGNABLE() != null ? ctx.ASSIGNABLE() - : ctx.MODIFIES() != null ? ctx.MODIFIES() : ctx.MODIFIABLE(); final boolean isFree = - assign != null && assign.getText().endsWith("_free"); + ctx.ASSIGNABLE() != null && ctx.ASSIGNABLE().getText().endsWith("_free"); final LabeledParserRuleContext ctx2 = LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree ? OriginTermLabel.SpecType.ASSIGNABLE_FREE @@ -281,11 +279,8 @@ public Object visitAssignable_clause(JmlParser.Assignable_clauseContext ctx) { @Override public Object visitLoop_assignable_clause(JmlParser.Loop_assignable_clauseContext ctx) { Name[] heaps = visitTargetHeap(ctx.targetHeap()); - final TerminalNode assign = ctx.ASSIGNABLE() != null ? ctx.ASSIGNABLE() - : ctx.MODIFIES() != null ? ctx.MODIFIES() - : ctx.MODIFIABLE() != null ? ctx.MODIFIABLE() : ctx.LOOP_ASSIGNABLE(); final boolean isFree = - assign != null && assign.getText().endsWith("_free"); + ctx.ASSIGNABLE() != null && ctx.ASSIGNABLE().getText().endsWith("_free"); final LabeledParserRuleContext ctx2 = LabeledParserRuleContext.createLabeledParserRuleContext(ctx, isFree ? OriginTermLabel.SpecType.ASSIGNABLE_FREE From c69175996bcd3e24412cdf3ede76b2af2ccd0d78 Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Thu, 29 Feb 2024 18:01:30 +0100 Subject: [PATCH 11/42] Some syntax harmonization for some consistency within the code base --- .../uka/ilkd/key/util/rifl/RIFLHandler.java | 8 +- .../de.uka.ilkd.key.util/rifl/rifl-1.0.dtd | 6 +- .../TestSymbolicExecutionTreeBuilder.java | 24 ++-- .../TestTruthValueEvaluationUtil.java | 24 ++-- .../slicing/TestThinBackwardSlicer.java | 36 ++--- .../de/uka/ilkd/key/testgen/ProofInfo.java | 4 +- .../ilkd/key/testgen/TestCaseGenerator.java | 2 +- key.core/src/main/antlr4/JmlLexer.g4 | 6 +- key.core/src/main/antlr4/JmlParser.g4 | 8 +- .../ilkd/key/logic/label/OriginTermLabel.java | 8 +- .../init/FunctionalOperationContractPO.java | 2 +- .../key/proof/init/WellDefinednessPO.java | 2 +- .../metaconstruct/CreateBeforeLoopUpdate.java | 2 +- .../rule/metaconstruct/CreateFrameCond.java | 2 +- .../metaconstruct/CreateHeapAnonUpdate.java | 4 +- .../AbstractAuxiliaryContractImpl.java | 26 ++-- .../ilkd/key/speclang/AuxiliaryContract.java | 10 +- .../ilkd/key/speclang/BlockContractImpl.java | 8 +- .../key/speclang/BlockWellDefinedness.java | 12 +- .../key/speclang/ClassWellDefinedness.java | 12 +- .../de/uka/ilkd/key/speclang/Contract.java | 2 +- .../key/speclang/DependencyContractImpl.java | 2 +- .../speclang/FunctionalAuxiliaryContract.java | 4 +- .../FunctionalOperationContractImpl.java | 6 +- .../speclang/InformationFlowContractImpl.java | 2 +- .../ilkd/key/speclang/LoopContractImpl.java | 20 +-- .../key/speclang/LoopWellDefinedness.java | 12 +- .../key/speclang/MethodWellDefinedness.java | 18 +-- .../speclang/StatementWellDefinedness.java | 6 +- .../key/speclang/WellDefinednessCheck.java | 66 +++++----- .../key/speclang/jml/JMLSpecExtractor.java | 4 +- .../pretranslation/TextualJMLLoopSpec.java | 30 ++--- .../pretranslation/TextualJMLSpecCase.java | 14 +- .../jml/translation/JMLSpecFactory.java | 124 +++++++++--------- .../key/speclang/njml/ContractClauses.java | 2 +- .../key/speclang/njml/JmlTermFactory.java | 10 +- .../key/speclang/njml/TextualTranslator.java | 26 ++-- .../ilkd/key/speclang/njml/Translator.java | 12 +- .../key/speclang/ContractFactoryTest.java | 6 +- .../speclang/jml/TestJMLPreTranslator.java | 10 +- .../ilkd/key/gui/sourceview/JavaDocument.java | 5 +- .../ilkd/key/gui/sourceview/SourceView.java | 2 +- 42 files changed, 295 insertions(+), 294 deletions(-) diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java index 94addf6468f..f7a7066bbb7 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java +++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java @@ -102,12 +102,12 @@ private void assignHandle(Attributes attributes) { categories2domains.put(p, domain); } - private void setAssignable(Attributes attributes) { + private void setModifiable(Attributes attributes) { assert tmpHandle == null; tmpHandle = attributes.getValue("handle"); } - private void unsetAssignable() { + private void unsetModifiable() { assert tmpHandle != null; tmpHandle = null; } @@ -214,7 +214,7 @@ public void startElement(String uri, String localName, String qName, Attributes // case "domainassignment": case "domains" -> startDomains(); case "domain" -> putDomain(attributes); - case "assignable" -> setAssignable(attributes); + case "modifiable" -> setModifiable(attributes); case "field" -> putField(attributes); case "parameter" -> putParam(attributes); case "returnvalue" -> putReturn(attributes); @@ -240,7 +240,7 @@ public void startElement(String uri, String localName, String qName, Attributes @Override public void endElement(String uri, String localName, String qName) { switch (localName) { - case "assignable" -> unsetAssignable(); + case "modifiable" -> unsetModifiable(); case "category" -> unsetCategory(); case "domains" -> checkDomains(); case "domainassignment" -> checkDomainAssignmentsWithFlows(); diff --git a/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/rifl-1.0.dtd b/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/rifl-1.0.dtd index 9c4a9da821a..618a508badd 100644 --- a/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/rifl-1.0.dtd +++ b/key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/rifl-1.0.dtd @@ -8,9 +8,9 @@ - - - + + + diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java index 606c82e328e..ef4d66447d4 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java @@ -186,37 +186,37 @@ public void testUseOperationContractLightweightOperationContractTest() throws Ex } /** - * Tests example: /set/blockContractAssignableEverything + * Tests example: /set/blockContractModifiableEverything */ @Test - public void testBlockContractAssignableEverything() throws Exception { + public void testBlockContractModifiableEverything() throws Exception { doSETTestAndDispose(testCaseDirectory, - "/set/blockContractAssignableEverything/test/BlockContractAssignableEverything.proof", - "/set/blockContractAssignableEverything/oracle/BlockContractAssignableEverything.xml", + "/set/blockContractModifiableEverything/test/BlockContractModifiableEverything.proof", + "/set/blockContractModifiableEverything/oracle/BlockContractModifiableEverything.xml", false, false, true, true, false, false, false, false, false, false, false, false, false); } /** - * Tests example: /set/blockContractAssignableLocationNotRequested + * Tests example: /set/blockContractModifiableLocationNotRequested */ @Test - public void testBlockContractAssignableLocationNotRequested() throws Exception { + public void testBlockContractModifiableLocationNotRequested() throws Exception { doSETTestAndDispose(testCaseDirectory, - "/set/blockContractAssignableLocationNotRequested/test/BlockContractAssignableLocationNotRequested.proof", - "/set/blockContractAssignableLocationNotRequested/oracle/BlockContractAssignableLocationNotRequested.xml", + "/set/blockContractModifiableLocationNotRequested/test/BlockContractModifiableLocationNotRequested.proof", + "/set/blockContractModifiableLocationNotRequested/oracle/BlockContractModifiableLocationNotRequested.xml", false, false, true, true, false, false, false, false, false, false, false, false, false); } /** - * Tests example: /set/blockContractAssignableRequestedLocation + * Tests example: /set/blockContractModifiableRequestedLocation */ @Test - public void testBlockContractAssignableRequestedLocation() throws Exception { + public void testBlockContractModifiableRequestedLocation() throws Exception { doSETTestAndDispose(testCaseDirectory, - "/set/blockContractAssignableRequestedLocation/test/BlockContractAssignableRequestedLocation.proof", - "/set/blockContractAssignableRequestedLocation/oracle/BlockContractAssignableRequestedLocation.xml", + "/set/blockContractModifiableRequestedLocation/test/BlockContractModifiableRequestedLocation.proof", + "/set/blockContractModifiableRequestedLocation/oracle/BlockContractModifiableRequestedLocation.xml", false, false, true, true, false, false, false, false, false, false, false, false, false); } diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java index 587c44c4811..e02a1979ce7 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestTruthValueEvaluationUtil.java @@ -89,10 +89,10 @@ public void testTruthValueLabelBelowUpdatesDifferentToApplicationTerm() throws E } /** - * Tests example: /set/truthValueExceptinalAssignableNothingTest + * Tests example: /set/truthValueExceptionalModifiableNothingTest */ @Test - public void testExceptinalAssignableNothingTest_OSS() throws Exception { + public void testExceptionalModifiableNothingTest_OSS() throws Exception { // Create expected results ExpectedBranchResult goal374 = new ExpectedBranchResult(new ExpectedTruthValueResult("0.0", TruthValue.FALSE), @@ -138,16 +138,16 @@ public void testExceptinalAssignableNothingTest_OSS() throws Exception { new ExpectedTruthValueEvaluationResult(goal374, goal407, goal444, goal475, goal476); // Perform test doTruthValueEvaluationTest( - "/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest_OSS.proof", - "/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml", + "/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest_OSS.proof", + "/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml", false, false, false, exceptionResult); } /** - * Tests example: /set/truthValueExceptinalAssignableNothingTest + * Tests example: /set/truthValueExceptionalModifiableNothingTest */ @Test - public void testExceptinalAssignableNothingTest() throws Exception { + public void testExceptionalModifiableNothingTest() throws Exception { // Create expected results ExpectedBranchResult goal374 = new ExpectedBranchResult(new ExpectedTruthValueResult("0.0", TruthValue.FALSE), @@ -193,8 +193,8 @@ public void testExceptinalAssignableNothingTest() throws Exception { new ExpectedTruthValueEvaluationResult(goal374, goal407, goal444, goal475, goal476); // Perform test doTruthValueEvaluationTest( - "/set/truthValueExceptinalAssignableNothingTest/test/ExceptinalAssignableNothingTest.proof", - "/set/truthValueExceptinalAssignableNothingTest/oracle/ExceptinalAssignableNothingTest.xml", + "/set/truthValueExceptionalModifiableNothingTest/test/ExceptionalModifiableNothingTest.proof", + "/set/truthValueExceptionalModifiableNothingTest/oracle/ExceptionalModifiableNothingTest.xml", false, false, false, exceptionResult); } @@ -310,11 +310,11 @@ public void IGNORE_testAddingOfLabeledSubtree() throws Exception { } /** - * Tests example: /set/truthValueAssignableAndLoop + * Tests example: /set/truthValueModifiableAndLoop */ @Test @Disabled - public void IGNORE_testAssignableAndLoop() throws Exception { + public void IGNORE_testModifiableAndLoop() throws Exception { // Create expected results ExpectedBranchResult goal430 = new ExpectedBranchResult(new ExpectedTruthValueResult("3.0", TruthValue.FALSE), @@ -370,8 +370,8 @@ public void IGNORE_testAssignableAndLoop() throws Exception { ExpectedTruthValueEvaluationResult result5 = new ExpectedTruthValueEvaluationResult(goal1113, goal1134, goal1137); // Perform test - doTruthValueEvaluationTest("/set/truthValueAssignableAndLoop/test/MagicProofNoOSS.proof", - "/set/truthValueAssignableAndLoop/oracle/MagicProofNoOSS.xml", true, true, false, + doTruthValueEvaluationTest("/set/truthValueModifiableAndLoop/test/MagicProofNoOSS.proof", + "/set/truthValueModifiableAndLoop/oracle/MagicProofNoOSS.xml", true, true, false, resultExceptionBranch, resultInvInitial, resultPrecondition, resultLoopEnd, result5); } diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java index 89abfcd9b27..3cca929d806 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/slicing/TestThinBackwardSlicer.java @@ -51,74 +51,74 @@ public class TestThinBackwardSlicer extends AbstractSymbolicExecutionTestCase { private static final Logger LOGGER = LoggerFactory.getLogger(TestThinBackwardSlicer.class); /** - * Tests slicing on the example {@code blockContractAssignableLocationNotRequested}. + * Tests slicing on the example {@code blockContractModifiableLocationNotRequested}. * * @throws Exception Occurred Exception. */ @Test - public void testBlockContractAssignableLocationNotRequested() throws Exception { + public void testBlockContractModifiableLocationNotRequested() throws Exception { doSlicingTest( - "/slicing/blockContractAssignableLocationNotRequested/BlockContractAssignableLocationNotRequested.proof", + "/slicing/blockContractModifiableLocationNotRequested/BlockContractModifiableLocationNotRequested.proof", new ReturnSelector(122), true, 109, 14, 12); } /** - * Tests slicing on the example {@code blockContractAssignableRequestedLocation}. + * Tests slicing on the example {@code blockContractModifiableRequestedLocation}. * * @throws Exception Occurred Exception. */ @Test - public void testBlockContractAssignableRequestedLocation() throws Exception { + public void testBlockContractModifiableRequestedLocation() throws Exception { doSlicingTest( - "/slicing/blockContractAssignableRequestedLocation/BlockContractAssignableRequestedLocation.proof", + "/slicing/blockContractModifiableRequestedLocation/BlockContractModifiableRequestedLocation.proof", new ReturnSelector(111), true, 23); } /** - * Tests slicing on the example {@code blockContractAssignableEverything}. + * Tests slicing on the example {@code blockContractModifiableEverything}. * * @throws Exception Occurred Exception. */ @Test - public void testBlockContractAssignableEverything() throws Exception { + public void testBlockContractModifiableEverything() throws Exception { doSlicingTest( - "/slicing/blockContractAssignableEverything/BlockContractAssignableEverything.proof", + "/slicing/blockContractModifiableEverything/BlockContractModifiableEverything.proof", new ReturnSelector(97), true, 23); } /** - * Tests slicing on the example {@code methodContractAssignableLocationNotRequested}. + * Tests slicing on the example {@code methodContractModifiableLocationNotRequested}. * * @throws Exception Occurred Exception. */ @Test - public void testMethodContractAssignableLocationNotRequested() throws Exception { + public void testMethodContractModifiableLocationNotRequested() throws Exception { doSlicingTest( - "/slicing/methodContractAssignableLocationNotRequested/MethodContractAssignableLocationNotRequested.proof", + "/slicing/methodContractModifiableLocationNotRequested/MethodContractModifiableLocationNotRequested.proof", new ReturnSelector(29), true, 14, 12); } /** - * Tests slicing on the example {@code methodContractAssignableRequestedLocation}. + * Tests slicing on the example {@code methodContractModifiableRequestedLocation}. * * @throws Exception Occurred Exception. */ @Test - public void testMethodContractAssignableRequestedLocation() throws Exception { + public void testMethodContractModifiableRequestedLocation() throws Exception { doSlicingTest( - "/slicing/methodContractAssignableRequestedLocation/MethodContractAssignableRequestedLocation.proof", + "/slicing/methodContractModifiableRequestedLocation/MethodContractModifiableRequestedLocation.proof", new ReturnSelector(29), true, 23); } /** - * Tests slicing on the example {@code methodContractAssignableEverything}. + * Tests slicing on the example {@code methodContractModifiableEverything}. * * @throws Exception Occurred Exception. */ @Test - public void testMethodContractAssignableEverything() throws Exception { + public void testMethodContractModifiableEverything() throws Exception { doSlicingTest( - "/slicing/methodContractAssignableEverything/MethodContractAssignableExample.proof", + "/slicing/methodContractModifiableEverything/MethodContractModifiableExample.proof", new ReturnSelector(29), true, 23); } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java index cc140fd6171..7c2ac9f4a98 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java @@ -86,9 +86,9 @@ public Term getPreConTerm() { return services.getTermBuilder().ff(); } - public Term getAssignable() { + public Term getModifiable() { Contract c = getContract(); - return c.getAssignable(services.getTypeConverter().getHeapLDT().getHeap()); + return c.getModifiable(services.getTypeConverter().getHeapLDT().getHeap()); } public String getCode() { diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java index e9b17899bd5..c1466476515 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java @@ -460,7 +460,7 @@ protected String getOracleAssertion(List oracleMethods) { oracleMethods.addAll(oracleGenerator.getOracleMethods()); LOGGER.debug("Modifier Set: {}", - oracleGenerator.getOracleLocationSet(info.getAssignable())); + oracleGenerator.getOracleLocationSet(info.getModifiable())); return "assertTrue(" + oracleCall + ");"; } diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index 002c9d5896d..4ca18aa0bca 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -74,11 +74,11 @@ fragment Pfree: '_free'?; //suffix ACCESSIBLE: 'accessible' Pred -> pushMode(expr); ASSERT: 'assert' Pred -> pushMode(expr); ASSUME: 'assume' Pred -> pushMode(expr); -ASSIGNABLE +MODIFIABLE : ('assignable' | 'assigns' | 'assigning' | 'modifiable' | 'modifies' | 'modifying' | 'writable' | 'writes' | 'writing') (Pfree|Pred) -> pushMode(expr); -LOOP_ASSIGNABLE +LOOP_MODIFIABLE : ('loop_assignable' | 'loop_assigns' | 'loop_assigning' | 'loop_modifiable' | 'loop_modifies' | 'loop_modifying' | 'loop_writable' | 'loop_writes' | 'loop_writing') (Pfree|Pred) -> pushMode(expr); @@ -181,7 +181,7 @@ DEPENDS: 'depends'; // internal translation for 'accessible' on model fields /* JML and JML* keywords */ /*ACCESSIBLE: 'accessible'; -ASSIGNABLE: 'assignable'; +MODIFIABLE: 'modifiable'; BREAKS: 'breaks'; CONTINUES: 'continues'; DECREASES: 'decreases'; // internal translation for 'measured_by' diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index 804323c5cc5..1449567d14d 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -65,7 +65,7 @@ clause : ( ensures_clause | requires_clause | measured_by_clause | captures_clause | diverges_clause | working_space_clause - | duration_clause | when_clause | assignable_clause | accessible_clause + | duration_clause | when_clause | modifiable_clause | accessible_clause | signals_clause | signals_only_clause | variant_function | name_clause | breaks_clause | continues_clause | returns_clause | separates_clause | determines_clause @@ -87,7 +87,7 @@ accessible_clause (lhs=expression COLON)? rhs=storeRefUnion (MEASURED_BY mby=expression)? SEMI_TOPLEVEL; -assignable_clause: ASSIGNABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; +modifiable_clause: MODIFIABLE targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; //depends_clause: DEPENDS expression COLON storeRefUnion (MEASURED_BY expression)? ; //decreases_clause: DECREASES termexpression (COMMA termexpression)*; represents_clause @@ -174,11 +174,11 @@ loop_specification | determines_clause | loop_separates_clause | loop_determines_clause - | loop_assignable_clause + | loop_modifiable_clause | variant_function)*; loop_invariant: LOOP_INVARIANT targetHeap? expression SEMI_TOPLEVEL; -loop_assignable_clause: (LOOP_ASSIGNABLE | ASSIGNABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; +loop_modifiable_clause: (LOOP_MODIFIABLE | MODIFIABLE) targetHeap? (storeRefUnion | STRICTLY_NOTHING) SEMI_TOPLEVEL; variant_function: DECREASING expression (COMMA expression)* SEMI_TOPLEVEL; //loop_separates_clause: SEPARATES expression; //loop_determines_clause: DETERMINES expression; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java index 5adc7067338..9fb36aa9062 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java @@ -782,14 +782,14 @@ public enum SpecType { ASSERT("assert"), /** - * assignable + * modifiable */ - ASSIGNABLE("assignable"), + MODIFIABLE("modifiable"), /** - * assignable_free + * modifiable_free */ - ASSIGNABLE_FREE("assignable_free"), + MODIFIABLE_FREE("modifiable_free"), /** * assume diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java index b00fe7b6233..8e19fe5a5ef 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java @@ -255,7 +255,7 @@ protected Term buildFrameClause(List modHeaps, Map } } - return tb.addLabelToAllSubs(frameTerm, new Origin(SpecType.ASSIGNABLE)); + return tb.addLabelToAllSubs(frameTerm, new Origin(SpecType.MODIFIABLE)); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java index 474bca4516d..a5177213160 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java @@ -39,7 +39,7 @@ * WD( && ) & * ( & * -> WD() & - * {anon^assignable}WD() + * {anon^modifiable}WD() * } * *

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java index f80b447495b..d9dd5bc891b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java @@ -15,7 +15,7 @@ import de.uka.ilkd.key.util.MiscTools; /** - * Initializes the "before loop" update needed for the assignable clause. + * Initializes the "before loop" update needed for the modifiable clause. * * Only remembers the heaps of the context, not the changed local variables, although this is done * for the built-in loop invariant rules, where they however are never used. diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java index b213c770edf..135e1a85745 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java @@ -23,7 +23,7 @@ import de.uka.ilkd.key.util.MiscTools; /** - * Creates the frame condition (aka "assignable clause") for the given loop. Also accepts the + * Creates the frame condition (aka "modifiable clause") for the given loop. Also accepts the * pre-state update and extracts the symbols from there. New symbols in the pre-state update (like * "heap_BeforeLOOP") are added to the namespaces. This is because the update is, for the loop scope * invariant taclet, created by a variable condition; new symbols created there are not diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateHeapAnonUpdate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateHeapAnonUpdate.java index d260b6b73f8..bfaea15b0ea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateHeapAnonUpdate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateHeapAnonUpdate.java @@ -77,10 +77,10 @@ private static Term createHeapAnonUpdate(LoopSpecification loopSpec, boolean isT final List heapContext = // HeapContext.getModHeaps(services, isTransaction); final Map mods = new LinkedHashMap<>(); - // The call to MiscTools.removeSingletonPVs removes from the assignable clause + // The call to MiscTools.removeSingletonPVs removes from the modifiable clause // the program variables which of course should not be part of an anonymizing // heap expression. The reason why they're there at all is that for Abstract - // Execution, it actually makes sense to have program variables in assignable + // Execution, it actually makes sense to have program variables in modifiable // clauses, since for an abstract statement they cannot be extracted like for // concrete statements (such as loop bodies). (DS, 2019-07-05) heapContext.forEach(heap -> mods.put(heap, diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java index 1cb413878ca..7bd04738279 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java @@ -571,7 +571,7 @@ public IProgramMethod getTarget() { } @Override - public Term getAssignable(LocationVariable heap) { + public Term getModifiable(LocationVariable heap) { return modifiesClauses.get(heap); } @@ -1020,14 +1020,14 @@ protected static abstract class Creator extends Ter private final Term diverges; /** - * A map from every heap to an assignable term. + * A map from every heap to an modifiable term. */ - private final Map assignables; + private final Map modifiables; /** - * A map from every heap to a free assignable term. + * A map from every heap to a free modifiable term. */ - private final Map assignablesFree; + private final Map modifiablesFree; /** * A list of heaps used in this contract. @@ -1066,8 +1066,8 @@ protected static abstract class Creator extends Ter * termination. * @param signalsOnly a term specifying which uncaught exceptions may occur. * @param diverges a diverges clause. - * @param assignables map from every heap to an assignable term. - * @param assignablesFree map from every heap to a free assignable term. + * @param modifiables map from every heap to an modifiable term. + * @param modifiablesFree map from every heap to a free modifiable term. * @param hasMod map specifying on which heaps this contract has a modifies clause. * @param hasFreeMod map specifying on which heaps this contract has a free modifies clause. * @param services services. @@ -1081,8 +1081,8 @@ public Creator(final String baseName, final StatementBlock block, final List infFlowSpecs, final Map breaks, final Map continues, final Term returns, final Term signals, final Term signalsOnly, final Term diverges, - final Map assignables, - final Map assignablesFree, + final Map modifiables, + final Map modifiablesFree, final Map hasMod, final Map hasFreeMod, final Services services) { @@ -1105,8 +1105,8 @@ public Creator(final String baseName, final StatementBlock block, final List buildModifiesClauses() { - return assignables; + return modifiables; } /** @@ -1436,7 +1436,7 @@ private Map buildModifiesClauses() { * @return the contract's free modifies clauses. */ private Map buildFreeModifiesClauses() { - return assignablesFree; + return modifiablesFree; } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java index 9307017e160..7f0646a25f0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java @@ -436,9 +436,9 @@ Term getFreeModifiesClause(LocationVariable heapVariable, Term heap, Term self, /** * * @param heap the heap to use. - * @return this contract's assignable term on the specified heap. + * @return this contract's modifiable term on the specified heap. */ - Term getAssignable(LocationVariable heap); + Term getModifiable(LocationVariable heap); /** * Accepts a visitor. @@ -656,7 +656,7 @@ class Variables { public final Map remembranceHeaps; /** - * A map from every variable {@code var} that is assignable inside the block to + * A map from every variable {@code var} that is modifiable inside the block to * {@code var_Before_BLOCK}. */ public final Map remembranceLocalVariables; @@ -693,7 +693,7 @@ class Variables { * @param exception exception variable to set when the block terminates by an uncaught * {@code throw} statement. * @param remembranceHeaps a map from every heap {@code heap} to {@code heap_Before_BLOCK}. - * @param remembranceLocalVariables a map from every variable {@code var} that is assignable + * @param remembranceLocalVariables a map from every variable {@code var} that is modifiable * inside the block to {@code var_Before_BLOCK}. * @param outerRemembranceHeaps a map from every heap {@code heap} that is accessible inside * the block to {@code heap_Before_METHOD}. @@ -1302,7 +1302,7 @@ class Terms { * @param exception exception variable to set when the block terminates by an uncaught * {@code throw} statement. * @param remembranceHeaps a map from every heap {@code heap} to {@code heap_Before_BLOCK}. - * @param remembranceLocalVariables a map from every variable {@code var} that is assignable + * @param remembranceLocalVariables a map from every variable {@code var} that is modifiable * inside the block to {@code var_Before_BLOCK}. * @param outerRemembranceHeaps a map from every heap {@code heap} that is accessible inside * the block to {@code heap_Before_METHOD}. diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java index c99f2a643e9..051c062ad17 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java @@ -242,7 +242,7 @@ public static class Creator extends AbstractAuxiliaryContractImpl.Creator labels, Term measuredBy, Map ensures, Map ensuresFree, ImmutableList infFlowSpecs, Map breaks, Map continues, Term returns, Term signals, - Term signalsOnly, Term diverges, Map assignables, - Map assignablesFree, + Term signalsOnly, Term diverges, Map modifiables, + Map modifiablesFree, Map hasMod, Map hasFreeMod, Services services) { super(baseName, block, labels, method, behavior, variables, requires, requiresFree, measuredBy, ensures, ensuresFree, infFlowSpecs, breaks, continues, returns, signals, signalsOnly, - diverges, assignables, assignablesFree, hasMod, hasFreeMod, services); + diverges, modifiables, modifiablesFree, hasMod, hasFreeMod, services); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java index eb975315251..e1bc7f2bcb8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java @@ -31,10 +31,10 @@ public class BlockWellDefinedness extends StatementWellDefinedness { private final BlockContract block; private BlockWellDefinedness(String name, int id, Type type, IObserverFunction target, - LocationVariable heap, OriginalVariables origVars, Condition requires, Term assignable, + LocationVariable heap, OriginalVariables origVars, Condition requires, Term modifiable, Term accessible, Condition ensures, Term mby, Term rep, BlockContract block, TermBuilder tb) { - super(name, id, type, target, heap, origVars, requires, assignable, accessible, ensures, + super(name, id, type, target, heap, origVars, requires, modifiable, accessible, ensures, mby, rep, tb); this.block = block; } @@ -55,7 +55,7 @@ public BlockWellDefinedness(BlockContract block, BlockContract.Variables variabl final LocationVariable h = getHeap(); this.block = block; setRequires(block.getPrecondition(h, variables, services)); - setAssignable(block.hasModifiesClause(h) ? block.getAssignable(h) : TB.strictlyNothing(), + setModifiable(block.hasModifiesClause(h) ? block.getModifiable(h) : TB.strictlyNothing(), services); setEnsures(block.getPostcondition(h, variables, services)); } @@ -63,7 +63,7 @@ public BlockWellDefinedness(BlockContract block, BlockContract.Variables variabl @Override public BlockWellDefinedness map(UnaryOperator op, Services services) { return new BlockWellDefinedness(getName(), id(), type(), getTarget(), getHeap(), - getOrigVars(), getRequires().map(op), op.apply(getAssignable()), + getOrigVars(), getRequires().map(op), op.apply(getModifiable()), op.apply(getAccessible()), getEnsures().map(op), op.apply(getMby()), op.apply(getRepresents()), block.map(op, services), services.getTermBuilder()); } @@ -89,14 +89,14 @@ public boolean transactionApplicableContract() { @Override public Contract setID(int newId) { return new BlockWellDefinedness(getName(), newId, type(), getTarget(), getHeap(), - getOrigVars(), getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(), + getOrigVars(), getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(), getRepresents(), getStatement(), TB); } @Override public Contract setTarget(KeYJavaType newKJT, IObserverFunction newPM) { return new BlockWellDefinedness(getName(), id(), type(), newPM, getHeap(), getOrigVars(), - getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(), + getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(), getRepresents(), getStatement().setTarget(newKJT, newPM), TB); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java index 6a26c9dbb00..97e0f4324f2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java @@ -33,10 +33,10 @@ public final class ClassWellDefinedness extends WellDefinednessCheck { private final ClassInvariant inv; private ClassWellDefinedness(String name, int id, Type type, IObserverFunction target, - LocationVariable heap, OriginalVariables origVars, Condition requires, Term assignable, + LocationVariable heap, OriginalVariables origVars, Condition requires, Term modifiable, Term accessible, Condition ensures, Term mby, Term rep, ClassInvariant inv, TermBuilder tb) { - super(name, id, type, target, heap, origVars, requires, assignable, accessible, ensures, + super(name, id, type, target, heap, origVars, requires, modifiable, accessible, ensures, mby, rep, tb); this.inv = inv; } @@ -48,7 +48,7 @@ public ClassWellDefinedness(ClassInvariant inv, IObserverFunction target, Term a assert inv != null; this.inv = inv; setRequires(inv.getOriginalInv()); - setAssignable(TB.strictlyNothing(), services); + setModifiable(TB.strictlyNothing(), services); setEnsures(inv.getOriginalInv()); setAccessible(accessible); setMby(mby); @@ -57,7 +57,7 @@ public ClassWellDefinedness(ClassInvariant inv, IObserverFunction target, Term a @Override public ClassWellDefinedness map(UnaryOperator op, Services services) { return new ClassWellDefinedness(getName(), id(), type(), getTarget(), getHeap(), - getOrigVars(), getRequires().map(op), op.apply(getAssignable()), + getOrigVars(), getRequires().map(op), op.apply(getModifiable()), op.apply(getAccessible()), getEnsures().map(op), op.apply(getMby()), op.apply(getRepresents()), inv.map(op, services), services.getTermBuilder()); } @@ -140,14 +140,14 @@ public boolean transactionApplicableContract() { @Override public ClassWellDefinedness setID(int newId) { return new ClassWellDefinedness(getName(), newId, type(), getTarget(), getHeap(), - getOrigVars(), getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(), + getOrigVars(), getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(), getRepresents(), getInvariant(), TB); } @Override public ClassWellDefinedness setTarget(KeYJavaType newKJT, IObserverFunction newPM) { return new ClassWellDefinedness(getName(), id(), type(), newPM, getHeap(), getOrigVars(), - getRequires(), getAssignable(), getAccessible(), getEnsures(), getMby(), + getRequires(), getModifiable(), getAccessible(), getEnsures(), getMby(), getRepresents(), getInvariant().setKJT(newKJT), TB); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/Contract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/Contract.java index 5fce4da8523..57e701167e4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/Contract.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/Contract.java @@ -149,7 +149,7 @@ Term getDep(LocationVariable heap, boolean atPre, Term heapTerm, Term selfTerm, Term getRequires(LocationVariable heap); - Term getAssignable(LocationVariable heap); + Term getModifiable(LocationVariable heap); Term getAccessible(ProgramVariable heap); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java index 254e116dfca..0716e5120b7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java @@ -238,7 +238,7 @@ public Term getRequires(LocationVariable heap) { } @Override - public Term getAssignable(LocationVariable heap) { + public Term getModifiable(LocationVariable heap) { throw new UnsupportedOperationException("Not applicable for dependency contracts."); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalAuxiliaryContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalAuxiliaryContract.java index 48c9f19fa0c..1368d978509 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalAuxiliaryContract.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalAuxiliaryContract.java @@ -246,8 +246,8 @@ public Term getRequires(LocationVariable heap) { } @Override - public Term getAssignable(LocationVariable heap) { - return contract.getAssignable(heap); + public Term getModifiable(LocationVariable heap) { + return contract.getModifiable(heap); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java index a34b12930fc..41c76640f68 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java @@ -69,11 +69,11 @@ public class FunctionalOperationContractImpl implements FunctionalOperationContr */ final Map originalAxioms; /** - * The original assignable clause terms. + * The original modifiable clause terms. */ final Map originalMods; /** - * The original assignable_free clause terms. + * The original modifiable_free clause terms. */ final Map originalFreeMods; final Map originalDeps; @@ -593,7 +593,7 @@ public Term getEnsures(LocationVariable heap) { } @Override - public Term getAssignable(LocationVariable heap) { + public Term getModifiable(LocationVariable heap) { return originalMods.get(heap); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java index 972089dcdbe..80ef9a56af8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java @@ -643,7 +643,7 @@ public Term getRequires(LocationVariable heap) { @Override - public Term getAssignable(LocationVariable heap) { + public Term getModifiable(LocationVariable heap) { return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java index ff2ae281ed4..9322cd366fa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java @@ -942,8 +942,8 @@ public static class Creator extends AbstractAuxiliaryContractImpl.Creator labels, Term measuredBy, Map ensures, Map ensuresFree, ImmutableList infFlowSpecs, Map breaks, Map continues, Term returns, Term signals, - Term signalsOnly, Term diverges, Map assignables, - Map assignablesFree, + Term signalsOnly, Term diverges, Map modifiables, + Map modifiablesFree, Map hasMod, Map hasFreeMod, Term decreases, Services services) { super(baseName, block, labels, method, behavior, variables, requires, requiresFree, measuredBy, ensures, ensuresFree, infFlowSpecs, breaks, continues, returns, signals, signalsOnly, - diverges, assignables, assignablesFree, hasMod, hasFreeMod, services); + diverges, modifiables, modifiablesFree, hasMod, hasFreeMod, services); this.decreases = decreases; } @@ -989,8 +989,8 @@ public Creator(String baseName, StatementBlock block, List