package java.util.concurrent;

/*@

predicate semaphore(real f, Semaphore s, int p, predicate() inv);

predicate create_semaphore_ghost_arg(predicate() inv) = true;

predicate n_times(int p, predicate() inv) = p == 0 ? emp : (inv() &*& n_times(p - 1, inv));

lemma void semaphore_dispose(Semaphore s);
    requires semaphore(1, s, ?p, ?inv);
    ensures n_times(p, inv);
    
lemma void semaphore_split_detailed(Semaphore s, real f1, int p1);
    requires semaphore(?f, s, ?p, ?inv) &*& 0 < f1 &*& f1 < f;
    ensures semaphore(f1, s, p1, inv) &*& semaphore(f - f1, s, p - p1, inv);

lemma void semaphore_split(Semaphore s);
    requires semaphore(?f, s, ?p, ?inv);
    ensures semaphore(f/2, s, 0, inv) &*& semaphore(f/2, s, p, inv);
    
lemma void semaphore_join();
    requires semaphore(?f1, ?s, ?p1, ?inv) &*& semaphore(?f2, s, ?p2, inv);
    ensures semaphore(f1 + f2, s, p1 + p2, inv);

@*/

public class Semaphore {
    Semaphore(int p);
        //@ requires n_times(p, ?inv);
        //@ ensures semaphore(1, this, p, inv);

    void acquire();
        //@ requires semaphore(?f, this, ?p, ?inv);
        //@ ensures semaphore(f, this, p - 1, inv) &*& inv();

    void release();
        //@ requires semaphore(?f, this, ?p, ?inv) &*& inv();
        //@ ensures semaphore(f, this, p + 1, inv);
}