1.2.2

got resolved as being a duplicate of #11

normally, constracts only make sense on public interfaces and not on private helper methods. Anyway, the candidate chec...

(from [18c82949d01f706051664a4c6e1e526b22cab920]) fixed [#22] and [#11] https://github.com/andresteingress/gcontracts/commit/18c82949d01f70...

normally, constracts only make sense on public interfaces and not on private helper methods. Anyway, the candidate check mechanism has been weakened to allow @R...

(from [18c82949d01f706051664a4c6e1e526b22cab920]) fixed [#22] and [#11] https://github.com/andresteingress/gcontracts/commit/18c82949d01f70...

(from [6370eff908b60883d98d65df754d181444ccc5ec]) added testcase for [#3] https://github.com/andresteingress/gcontracts/commit/6370eff908b608...

has been resolved due to work done in [#19]

(from [6a8a09ef78b5761337a9d594e22ffb726e9918f6]) test-case for [#16] https://github.com/andresteingress/gcontracts/commit/6a8a09ef78b576...

the problem is that getBalance() is user-defined. since it is user-defined it gets injected with a class invariant. the call in the class invariant gets compile...

(from [3a5962765b6baf077e0395beffeac5fabdba51fb]) multiple return statements cause missing postcondition validation [#19] https://github.com/andresteingress/gc...

@Invariant({ balance >= 0.0 })
class Account {

   protected double balance   

   def withdraw(BigDecimal amount) {
      balance -= amount
      return amoun...

(from [1bef314b0d4a872b53069e247eb91a94b88f74ce]) precondition specification on constructor with default value fails [#20] https://github.com/andresteingress/g...

(from [88df45de9607f46d3cdb8454c15f6abb4752c3b3]) precondition specification on constructor with default value fails [#20] https://github.com/andresteingress/g...

class BetterAccount extends Account {
    
    BigDecimal withdraw( BigDecimal amount )
    {
        if ((balance + frame) < amount) {
          return 0.0
  ...

let's consider this valid piece of precondition overriding:

class Account 
{
    protected BigDecimal balance

    def Account( BigDecimal amount = 0.0 )
    {...

the problem occurs only if the inherited class computes the old variables map, but the predecessor does not.

it seems that the old variable generation does not work on inherited instance variables:

import org.gcontracts.annotations.*

// by http://www.javacoffeebreak....

whenever an invariant is applied on some sort of the following method, the generated code calls the last statement twice

def pop() {
elements.pop() }

vs.

def po...

(from [918573359a0543efc899b12b5581d5e499dbce7d]) allow multiple labels in contracts [#15] https://github.com/andresteingress/gcontracts/commit/918573359a0543....

(from [d04bab17589b13934b58783d51cfd82d8e8575fe]) fixed usage of labels in @Requires, @Ensures and @ClassInvariant [#14] https://github.com/andresteingress/gco...

the following code should execute successfully

import org.gcontracts.annotations.*

@Invariant({
   never_be_null: internal_list != null
})
class Stack {
   d...

needs futher research to avoid cyclic calls on static methods - changes in CandidateChecks are trivial