Auction Theory Toolbox – Isabelle (generated Scala code)
Verified code generated from the Isabelle formalisation
- Source repository (on GitHub).
- all-in-one ZIP archive for download
- Self-contained demos:
- Hard-coded input: executable code, source
- Using the bid format of CATS: executable code, source, sample bid input
- Using a variant of the CATS format with bidder IDs (“CAB”): executable code, source, sample bid input
- Other shared code modules:
- TieBreaker.scala: tie-breaking functions
- Wrappers around various types of the Isabelle library to make them Scala-friendly:
- NatSetWrapper.scala:
nat set - RatWrapper.scala: rational numbers
- SetWrapper.scala:
set - IsabelleLibraryWrapper.scala: general functions
- NatSetWrapper.scala:
- Utilities:
- split-scala-modules.pl: splits Isabelle-generated Scala code into one Scala source file per module (i.e. per
object/class) - Makefile contains rules to regenerate some of the files mentioned above.
- split-scala-modules.pl: splits Isabelle-generated Scala code into one Scala source file per module (i.e. per
How to run
- For just executing the generated code, obtain Scala (see below), or use Java with a recent version of scala-library.jar, e.g. scala-library-2.10.2. Then follow the instructions in README.
- For building the code, obtain Isabelle and Scala. Our formalisation is known to work with Isabelle2013-1-RC1; the generated code is known to work with Scala 2.10.
- You currently need to manually load and run any of the Isabelle theories that generate code (check the overview for “code”), e.g. in jEdit.
- The Makefile has several relevant targets; e.g., you can build and run the CAB example as follows:
make CombinatorialVickreyAuctionCAB.classscala CombinatorialVickreyAuctionCAB < example.cab
- For executing split-scala-modules.pl (required by the Makefile), you need Perl ≥5.10 with the
File::Specmodule.
This page was last modified on 04 October 2013.