Error parsing nested updates

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

To understand the functionality of updates I have been playing around and found the following bug in parsing nested updates (easy to circumvent but nevertheless).

testFile.key:

\programVariables {
        int a,b;
}

\problem {
        a = 1 & b = 2
        -> 
        {{a:=3} b:=a}( a = 1 & b = 3 )
}

Parsing error (de.uka.ilkd.key.proof.init.ProofInputException):

Not a legal lhs: update-application(elem-update(a)(Z(3(#))),b)

  {{a:=3} b:=a}( a = 1 & b = 3 )
             ^

Stack trace:

de.uka.ilkd.key.proof.init.ProofInputException: Not a legal lhs: update-application(elem-update(a)(Z(3(#))),b)
	at de.uka.ilkd.key.proof.io.KeYFile.read(KeYFile.java:455)
	at de.uka.ilkd.key.proof.init.KeYUserProblemFile.read(KeYUserProblemFile.java:165)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.readEnvInput(ProblemInitializer.java:387)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:562)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:518)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:490)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:252)
	at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:78)
	at de.uka.ilkd.key.proof.io.ProblemLoader.access$000(ProblemLoader.java:38)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:124)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:117)
	at javax.swing.SwingWorker$1.call(SwingWorker.java:295)
	at java.util.concurrent.FutureTask.run(FutureTask.java:266)
	at javax.swing.SwingWorker.run(SwingWorker.java:334)
	at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
	at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
	at java.lang.Thread.run(Thread.java:748)
Caused by: /home/lukas/key/git/nestedUpdates2.key(8, 13): Not a legal lhs: update-application(elem-update(a)(Z(3(#))),b)
	at de.uka.ilkd.key.parser.KeYParser.elementary_update_term(KeYParser.java:5737)
	at de.uka.ilkd.key.parser.KeYParser.term(KeYParser.java:5603)
	at de.uka.ilkd.key.parser.KeYParser.updateterm(KeYParser.java:9266)
	at de.uka.ilkd.key.parser.KeYParser.braces_term(KeYParser.java:9001)
	at de.uka.ilkd.key.parser.KeYParser.term110(KeYParser.java:6830)
	at de.uka.ilkd.key.parser.KeYParser.strong_arith_op_term(KeYParser.java:6717)
	at de.uka.ilkd.key.parser.KeYParser.weak_arith_op_term(KeYParser.java:6636)
	at de.uka.ilkd.key.parser.KeYParser.logicTermReEntry(KeYParser.java:6542)
	at de.uka.ilkd.key.parser.KeYParser.equality_term(KeYParser.java:6167)
	at de.uka.ilkd.key.parser.KeYParser.term60(KeYParser.java:6040)
	at de.uka.ilkd.key.parser.KeYParser.conjunction_term(KeYParser.java:5950)
	at de.uka.ilkd.key.parser.KeYParser.disjunction_term(KeYParser.java:5886)
	at de.uka.ilkd.key.parser.KeYParser.implication_term(KeYParser.java:5828)
	at de.uka.ilkd.key.parser.KeYParser.implication_term(KeYParser.java:5843)
	at de.uka.ilkd.key.parser.KeYParser.equivalence_term(KeYParser.java:5764)
	at de.uka.ilkd.key.parser.KeYParser.elementary_update_term(KeYParser.java:5704)
	at de.uka.ilkd.key.parser.KeYParser.term(KeYParser.java:5603)
	at de.uka.ilkd.key.parser.KeYParser.formula(KeYParser.java:5563)
	at de.uka.ilkd.key.parser.KeYParser.problem(KeYParser.java:15207)
	at de.uka.ilkd.key.proof.io.KeYFile.read(KeYFile.java:435)
	... 16 more
Caused by: de.uka.ilkd.key.logic.TermCreationException: Not a legal lhs: update-application(elem-update(a)(Z(3(#))),b)
	at de.uka.ilkd.key.logic.TermBuilder.elementary(TermBuilder.java:959)
	at de.uka.ilkd.key.parser.KeYParser.elementary_update_term(KeYParser.java:5723)
	... 35 more

Circumvent with additional brackets around b:=a then everything is fine:

\programVariables {
        int a,b;
}

\problem {
        a = 1 & b = 2
        ->
        {{a:=3} (b:=a)}( a = 1 & b = 3 )
}

However, this is displayed in key without brackets as in the testFile:

 ==> a = 1 & b = 2 -> {{a:=3}b:=a}(a = 1 & b = 3)

Without pretty printing:

 ==> a = Z(1(#)) & b = Z(2(#)) -> {{a:=Z(3(#))}b:=a}(a = Z(1(#)) & b = Z(3(#)))

---

Information:

• created_at: 2020-06-09T11:05:57.723Z
• updated_at: 2020-10-14T01:52:24.174Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 10