@pre-functions in DL method contracts are not in namespace

[wadoon]

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

---

• Mantis: MT-731

• Submitted on: 2006-10-13 by (at)pruemmer

• Updated: 2006-12-17

• Assigned to: (at)bweiss

Description

When using a DL method contract (i.e., instead of expanding a method invocation) symbols ...(at)pre are introduced, but are not added to the functions namespace and cannot be entered/parsed in the instantiation dialog. A further problem seems to be that the names of such symbols are not made unique in a proper way, when using the same contract more than once multiple symbols ...(at)pre with the same name will be introduced.

Files

Notes

(at)rbubel at 2006-10-26

The first part of the bug (symbols not in namespace) has been fixed by Benjamins latest checkin.

edited on: 26-Oct-06 16:23

(at)pruemmer at 2006-12-07

fix is mandatory for 1.0

(at)bweiss at 2006-12-11

The second part (unique naming) apparently also has been fixed somewhere along the way. However, the introduced names of the form "name(at)pre1", "name(at)pre2", ... can't be parsed. As I didn't feel like changing the parser, I just changed the syntax to "nameAtPre1", "nameAtPre2",... in 0.2411.

Also, the symbols which were added to the functions namespace were not the same symbols which were actually used in the sequent. This is fixed in 0.2411, too.

(at)pruemmer at 2006-12-12

Thanks for fixing the bug and sorry that I just found a further place where the parsing does not work: when I start a correctness proof for a DL method contract (using the DL method contract browser), the (at)pre symbols used in the proof obligation can lead to unparseable formulas.
To reproduce this, load the file examples/java_dl/DLContractChooser/example.key, choose the "twenty" contract, and then try to cut in a formula containing the symbol MyClass::a(at)pre

(at)bweiss at 2006-12-13

Yes, and the same thing used to happen for OCL proof obligations, too. It's fixed in 0.2413.

History

• (at)pruemmer -- (NEW_BUG) 2006-10-13

• (at)rbubel -- (BUGNOTE_ADDED) 2006-10-26

• (at)rbubel -- (BUGNOTE_UPDATED) 2006-10-26

• (at)pruemmer -- (BUGNOTE_ADDED) 2006-12-07

• (at)pruemmer -- (NORMAL_TYPE) 2006-12-07

• (at)bweiss -- (NORMAL_TYPE) 2006-12-11

• (at)bweiss -- (NORMAL_TYPE) 2006-12-11

• (at)bweiss -- (NORMAL_TYPE) 2006-12-11

• (at)bweiss -- (NORMAL_TYPE) 2006-12-11

• (at)bweiss -- (BUGNOTE_ADDED) 2006-12-11

• (at)pruemmer -- (NORMAL_TYPE) 2006-12-12

• (at)pruemmer -- (NORMAL_TYPE) 2006-12-12

• (at)pruemmer -- (BUGNOTE_ADDED) 2006-12-12

• (at)bweiss -- (NORMAL_TYPE) 2006-12-13

• (at)bweiss -- (NORMAL_TYPE) 2006-12-13

• (at)bweiss -- (BUGNOTE_ADDED) 2006-12-13

• (at)pruemmer -- (NORMAL_TYPE) 2006-12-17

Attributes

• Category: GUI
• Status: CLOSED
• Severity: MINOR
• OS:
• Target Version:
• Resolution: FIXED
• Priority: URGENT
• Reproducibility: ALWAYS
• Platform:
• Commit: None
• Build: 0.2375
• Tags []
• Labels: ~GUI ~Bug ~URGENT

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:25:56.869Z
• updated_at: 2017-05-29T02:25:57.922Z
• closed_at: 2017-05-29T02:25:57.828Z (closed_by: )
• milestone:
• user_notes_count: 0