#Post condition does not hold

1 messages · Page 1 of 1 (latest)

spice swallow
# 
    /**
     * computes the echarge of this
     * @post | getAlphas().stream().anyMatch(el -> Math.abs(result) == el.getBalls().size())
     * @post | getAlphas().size() % 2 == 0 ? result > 0 : result < 0
     * @inspects | this
     */
    int regetEchargePkg() {
        int sig = alphaSizeToSign();
        int val = 1;
        for (Alpha alph : linkedAlphas) {
            if (alph.linkedBalls.size() > val) { val = alph.linkedBalls.size(); }
        }
        return sig * val;
    }

sig is the value 1 or -1. getBalls() and getAlphas() give respectively a shallow copy of linkedBalls and linkedAlphas. Any idea why the first post condition would not hold? If more information is needed pls ask. Thnx

mint dewBOT
#

⌛ This post has been reserved for your question.

Hey @spice swallow! Please use /close or the Close Post button above when you're finished. Please remember to follow the help guidelines. This post will be automatically closed after 300 minutes of inactivity.

TIP: Narrow down your issue to simple and precise questions to maximize the chance that others will reply in here.