post conditions not being generated.

[Paul]

I am using the Royal and Loyal example, and all the Java Code seems to be generating example for the post condition. For example:

context Customer::birthdayHappens()
  post: age = age@pre + 1

Does not produce anything

Neither does

context LoyaltyAccount::isEmpty(): Boolean
  pre : true -- none
  post: result = (points = 0)

I am using Octopus 2.2.0 with eclipse 3.1.2 and Java 5 Update 6.

[Jos Warmer]

You are quite right. Octopus does not generate code for postconditions. This choice has been made because of two reasons:
- it is _very_ hard to produce code for @pre expressions
- the added value of postcondition generation has proven to be niot that big.

Regards, Jos

[Paul]

That explains why I can't generate them :).