public class CarPark
{
    private int capacity;
    public int capacity () {return capacity;}
    
    private int carCount = 0;
	
    public CarPark (int initCapacity)
    {
        assert initCapacity > 0 : "Precondition: Initial value of capacity positive";
        capacity = initCapacity;
        assert 0 <= carCount && carCount <= capacity : "Class Invariant";
    }
	
    public synchronized void request () throws InterruptedException
    {
        assert 0 <= carCount && carCount <= capacity : "Class Invariant";
        while (carCount >= capacity)
        {
            try
            {
                wait();
            }
            catch(InterruptedException e)
            {
                throw new InterruptedException("request wait interrupted");
            }
        }
        ++carCount;
        System.out.println("Free places: " + (capacity - carCount));
        assert 0 <= carCount && carCount <= capacity : "Class Invariant";
        assert carCount > 0 : "Postcondition: #called(release) <= #completed(request)";
    }
	
    public synchronized void release ()
    {
        assert 0 <= carCount && carCount <= capacity : "Class Invariant";
        assert carCount > 0 : "Precondition: #called(release) <= #completed(request)";
        --carCount;
        notify();
        System.out.println("Free places: " + (capacity - carCount));
        assert 0 <= carCount && carCount <= capacity : "Class Invariant";
    }
}