OpenJML postcondition (and loop invariant) contains class method call

Question

I would like to call a class method in the postcondition (and loop invariant) of another method. The most relevant thing that I have found was this post in StackOverflow.

I tried to open the link which was provided there (http://www.ibm.com/developerworks/java/library/j-jml/index.html); however, it doesn't work anymore. 1- Is there any (other) resource that I can find “how to call a class method in postcondition of the other function”?

2- Once I tried to test the example there in OpenJML, I received an error for static verification:

enter image description here

Just I was able to use runtime assertion checking for this example:

enter image description here

Any help would be appreciated regarding calling a method in postcondition in static verification (or runtime assertion). Thank you

-- I am using openjml 0.17.0-alpha-9 on ubuntu 20.04.