A Coq-based synthesis of Scala programs which are correct-by-construction
GPL-3.0 License
First, download the Scala Build Tool (SBT) from http://www.scala-sbt.org/download.html
Then, in the project's main directory run the command sbt assembly
Finally, the below command:
scala target/scala-2.12/scallina-assembly-<scallina-version>.jar <path-to-coq-source-file.v>
can be executed from the project's main directory in order to run Scallina.
Also, the below command should also work:
java -jar target/scala-2.12/scallina-assembly-<scallina-version>.jar <path-to-coq-source-file.v>
Packaged examples are available under packaged-examples
Additional examples of Coq .v
files that can be translated to Scala are available under src/test/resources/
The generated files can be compiled with the scalac
Scala compiler provided that the Scallina Standard Library is included in the classpath.
For a practical example, see the compile-scala-code.sh
script in packaged-examples/v0.7.0/SelectionSort
.
The source code of the Scallina Standard Library is available under src/main/resources/scala/of/coq/lang
.