Public | Automated Build

Last pushed: 2 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 https://bitbucket.org/cogumbreiro/hj-why3; 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:

./docker-prove.sh

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):

./docker-prove.sh phasediff.why

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

Docker Pull Command
Owner
cogumbreiro
Source Repository