POs for constructors

[wadoon]

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

---

• Mantis: MT-907

• Submitted on: 2008-06-12 by (at)most

• Updated: 2012-03-09

• Assigned to: (at)bweiss

Description

Should be a bit different than for other methods I guess. I know that listing the contracts for is a temporary fix I requested, but it is misleading (and incorrect I guess) to, for example, have PreservesInv for . Also I think the invariant should not be assumed by default for an method.

Files

Notes

(at)bweiss at 2009-07-20

POs for constructors should make sense now, see fix for #702 (at least the usual trinity of EnsuresPost, PreservesInv and RespectsModifies).

History

• (at)most -- (NEW_BUG) 2008-06-12

• (at)bweiss -- (NORMAL_TYPE) 2009-07-20

• (at)bweiss -- (NORMAL_TYPE) 2009-07-20

• (at)bweiss -- (BUGNOTE_ADDED) 2009-07-20

• (at)bweiss -- (NORMAL_TYPE) 2009-07-20

• (at)bweiss -- (NORMAL_TYPE) 2009-07-20

• (at)grahl -- (BUG_ADD_RELATIONSHIP) 2011-11-28

• (at)most -- (NORMAL_TYPE) 2012-03-09

Attributes

• Category: Prover Core
• Status: CLOSED
• Severity: MINOR
• OS:
• Target Version:
• Resolution: FIXED
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: None
• Build: 1.3.X
• Tags []
• Labels: ~Prover Core ~Bug ~NORMAL

---

View in Mantis

---

Information:

• created_at: 2017-05-29T03:02:44.676Z
• updated_at: 2017-05-29T03:02:45.561Z
• closed_at: 2017-05-29T03:02:45.459Z (closed_by: )
• milestone:
• user_notes_count: 0