GeezerVison

The World Wide Web, restored to 800 pixels of glory.

GeezerVison is showing liquid-java.github.io — Counter

Counter

This example uses plain refinements on method parameters and return values to ensure a counter never decrements below zero.

import liquidjava.specification.Refinement;

public class Counter {
    @Refinement("_ == count + 1")
    public static int increment(@Refinement("count >= 0") int count) {
        return count + 1;
    }

    @Refinement("_ == count - 1")
    public static int decrement(@Refinement("count > 0") int count) {
        return count - 1;
    }
}

int c = 0;
c = Counter.increment(c);
c = Counter.decrement(c);
c = Counter.decrement(c); // Refinement Error

The parameter refinement on decrement requires the input to be strictly positive, so LiquidJava rejects the final call when c is already 0.

You are visitor 01402503 — GeezerVison does not store the pages you look up.
Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.