Public | Automated Build

Last pushed: 3 years ago
Short Description
HJ formalization in Why3
Full Description

Habanero-Java Why3 formalization

The following code formalizes the semantics of Phasers along with a property of deadlock avoidance.

Installing Docker on MacOSX

  1. Install VirtualBox

  2. Install Homebrew

  3. Install Docker: brew install docker git

  4. Clone our repository: git clone; cd hj-why3

  5. Open port 8080 of the docker installation

    VBoxManage modifyvm "boot2docker-vm" --natpf1 "tcp-port8000,tcp,,8080,,8080" || VBoxManage controlvm "boot2docker-vm" natpf1 "tcp-port8000,tcp,,8080,,8080";

Testing the formalization (Docker)

To check all proofs of available do:


To edit a single proof do, say phasediff.why do and follow the instructions once the application stalls (it should tell you to open the browser in http://localhost:8080):

./ phasediff.why

Note: the first time you run will automatically download an image, so it should take longer. Afterwards, running the test should be fast.

Docker Pull Command
Source Repository