Worthwhile is an application that makes proving simple programs accessible and fun! It was developed as a project for the course "Praxis der Softwareentwicklung" at the University of Karlsruhe at the Institute for Theoretical Informatics.
Z3 is a theorem prover developed by Microsoft Research. A recent build for Linux is available on their website. To be able to use Z3 from within Worthwhile, you can either put the Z3 binary in your $PATH (named z3) or enter the path manually in the Worthwhile preferences (Window → Preferences → Worthwhile → Path to Z3 binary).
Worthwhile is built on the Eclipse Platform. Java SE 6, Eclipse 3.7.1 and Maven 3 or later are required to build the project.
Worthwhile uses the Eclipse Xtext framework and the Xtext Typesystem framework. Therefore, to build a project, an Eclipse environment with these plugins installed is required. Itemis provides prebuilt Eclipse binaries with these plugins already installed on their website. The Xtext Typesystem plugins (Version 2.0-beta, available in the "Downloads" area of their Google Code page) should be placed in the plugins/ directory of your Eclipse installation.
The easiest way to run Worthwhile from source is launching it from within an existing Eclipse instance. Because for some reason, maven-eclipse-plugin requires all build artifacts to be in place when generating .project files for Eclipse, all projects have to be built and the build artifacts installed to the local Maven repository before generating the project files. If you have figured out a better way to do this, please let us know.
cd implementierung/src
mvn install -Dmaven.test.skip=true
mvn eclipse:eclipseAfter this step has completed, open Eclipse, select File → Import... → Existing Projects into Workspace and choose the implementierung/src directory. Import all the projects and wait for Eclipse to stabilize in flight.
You might also need to add com.google.inject as a dependency to the product. Find edu.kit.iti.formal.pse.worthwhile.product/META-INF/MANIFEST.MF, open it, select the Dependencies tab and add com.google.inject as a dependency.
Nobody knows why, but to get everything to work you have to open edu.kit.iti.formal.pse.worthwhile.product/worthwhile.product, select the Dependencies tab and press the Add Required Plug-ins button. Now, switch back to the Overview tab and in the Testing section first select Synchronize and then Launch an Eclipse application. Boom! You're in for endless hours of fun with Worthwhile!