Assertion failure: Call to non-existant constructor.

[wadoon]

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

---

• Mantis: MT-802

• Submitted on: 2007-03-07 by (at)pruemmer

• Updated: 2011-02-15

• Assigned to: (at)bweiss

Description

This happens when you try to verify "Assignable PO for Purity specification" for the example examples/BookExamples/chap10UsingKey/Bank-JML and the method bank.Account.Account(finalint
accountnumber)

Btw, why does a string "finalint" occur in the JML specification browser?

Files

Notes

(at)pruemmer at 2007-08-03

Another funny bug: in the proof obligation, formulas like

                \[{
                    bank.Account.new  bank.Account (accountNumber)
                  }\] x = o.accountNumber))

occur. Please note the missing semicolon ...

(at)pruemmer at 2007-08-03

Scheduled for Summer-of-69 release

(at)mulbrich at 2007-08-29

The problem is the following:
bank.Account is an abstract class and therefore lacks the implicit field which would be needed to resolve
account_2=bank.Account.()(at)bank.Account;

The proof obligation itself is questionable since the code
self_Account=new bank.Account (accountNumber);

is illegal as Account is abstract.

How could this be dealt with? Perhaps the PO should only talk about "Account.()" instead of the constructor?

edited on: 29-Aug-07 10:26

(at)rbubel at 2007-08-29

OK, we should then classify it as a specification error, which should be reported at the JML/OCL/JavaCardDL parsing stage.

(at)pruemmer at 2007-08-29

I think that the specification is correct, it is reasonable to specify stuff like "pure" also for the constructor of an abstract class. (and I do not think that JML forbids such specifications)

Not sure what the PO should actually express ... how is this problem handled for post-conditions of constructors of abstract classes? There has to be some concept for that as well. I think one mostly has to check the effect of the method, but then also the automatic initialisation of fields with 0, null, etc. has to be carried out (is this part of ?)

(at)mulbrich at 2007-08-29

The initialisation of the fields is done in () which is called from () during object creation.

So, it might be more appropriate to have a PO like
< self_Account.(); self_Account.(accountNumber); > phi

which does not make statements about the exact type of self_Account.

Perhaps this has to be done for non-abstract classes as well, since super-class constructors may be called using the "super(args)" statement.

(at)pruemmer at 2007-08-29

I guess the last point is only important if it is also possible to use the contracts for super-class constructors in proofs? (which should be possible, of course)

This makes sense, but one has to be careful when doing the same thing for checking post-conditions ... pre-/post-conditions of a constructor probably expect (and could express) that a new object has been created in between?

(at)mulbrich at 2007-08-29

It can expect and express that a new object of some subtype has been created, yet not of which exact type.

The following post-condition could not hold for a constructor, since there might be a class B <: A which calls "super()", not creating a new instance of A.

constructor A.A()
post: A. > \old(A.)

Would the invalidation of the -fields of all non-abstract subclasses have the desired effect?

(at)bweiss at 2009-07-20

The original assertion failure is long gone (new JML translation).

With the fix for #702, a consistent handling of constructor contracts should be in place. Note that we now interpret constructor contracts as contracts for only, so unlike what has been written here, the contract may not express that the object has been created between pre and post.

(at)bweiss at 2011-02-15

Closing as reporter is no longer available.

History

• (at)pruemmer -- (NEW_BUG) 2007-03-07

• (at)pruemmer -- (BUGNOTE_ADDED) 2007-08-03

• (at)pruemmer -- (BUGNOTE_ADDED) 2007-08-03

• (at)pruemmer -- (NORMAL_TYPE) 2007-08-03

• (at)mulbrich -- (BUGNOTE_ADDED) 2007-08-29

• (at)mulbrich -- (BUGNOTE_UPDATED) 2007-08-29

• (at)rbubel -- (BUGNOTE_ADDED) 2007-08-29

• (at)pruemmer -- (BUGNOTE_ADDED) 2007-08-29

• (at)mulbrich -- (BUGNOTE_ADDED) 2007-08-29

• (at)pruemmer -- (BUGNOTE_ADDED) 2007-08-29

• (at)mulbrich -- (BUGNOTE_ADDED) 2007-08-29

• (at)rbubel -- (NORMAL_TYPE) 2007-10-16

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

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

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

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

• (at)bweiss -- (BUGNOTE_ADDED) 2011-02-15

• (at)bweiss -- (NORMAL_TYPE) 2011-02-15

Attributes

• Category: Prover Core
• Status: CLOSED
• Severity: MAJOR
• OS:
• Target Version:
• Resolution: FIXED
• Priority: HIGH
• Reproducibility: ALWAYS
• Platform:
• Commit: None
• Build: 0.2534
• Tags []
• Labels: ~Prover Core ~Bug ~HIGH

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:54:53.626Z
• updated_at: 2017-05-29T02:54:56.375Z
• closed_at: 2017-05-29T02:54:56.338Z (closed_by: )
• milestone:
• user_notes_count: 0