package java.lang;

/*@

predicate_family thread_run_pre(Class c)(Runnable run, any info);
predicate_family thread_run_post(Class c)(Runnable run, any info);

@*/

public interface Runnable {
    public void run();
        //@ requires thread_run_pre(this.getClass())(this, ?info);
        //@ ensures thread_run_post(this.getClass())(this, info);
}

/*@

predicate thread(Thread thread, Runnable run);
predicate thread_started(Thread thread, Runnable run, any info);

@*/

public class Thread {
    public Thread(Runnable run);
        //@ requires true;
        //@ ensures thread(this, run);
    
    void start();
        //@ requires thread(this, ?run) &*& thread_run_pre(run.getClass())(run, ?info);
        //@ ensures thread_started(this, run, info);
}