This is the back-end API that services request to compile, translate and verification using the RESOLVE compiler. The project requires sbt 1.x
, Scala 2.13.x
, Java 8+
and Play Framework 2.8.x
to run. Instructions to install these requirements can be found on their respective websites.
RESOLVE (REusable SOftware Language with VErification) is a specification and programming language designed for verifying correctness of object oriented programs.
The RESOLVE language is designed from the ground up to facilitate mathematical reasoning. As such, the language provides syntactic slots for assertions such as pre-post conditions that are capable of abstractly describing a program's intended behavior. In writing these assertions, users are free to draw from a variety of pre-existing and user-defined mathematical theories containing fundamental axioms, definitions, and results necessary/useful in establishing program correctness.
All phases of the verification process spanning verification condition (VC) generation to proving are performed in-house, while RESOLVE programs are translated to Java and run on the JVM.
As a prerequisite, you will need to download and install sbt 1.x
and Java JDK 8+
. The current project is already configured to install Scala 2.13.x
, Play Framework
and all necessary plugins. Instructions on how to setup your favorite development IDE can be found here.
This project is similar to a typical Play Framework
project and follows the MVC
pattern. Only the important files are described in this section and shown in the figure below. See here for more information. All application source files are located inside the app
folder and the unit testing files are located in test
. The compiler
folder contains things that are needed to instantiate a compile job as well as how to handle input and output messages from the compiler. The controllers
and views
folders contain the controllers for the various different WebSocket
protocols and HTML
rendering template code. All static resources can be found in the public
directory.
The bin
folder contains integration scripts to be used by TravisCI
and should only be modified if any of the integration testing needs to be updated. Inside the conf
folder are various different settings to be used by the application
. This application
depends on a deployment-dependent local-config.conf
. More information on how to setup this file can be found in the following section.
RESOLVEWebAPI/
├── app/
│ ├── compiler
│ ├── controllers
│ ├── views
└── bin/
└── custom_lib/
└── conf/
└── project/
└── public/
│ ├── stylesheets
│ ├── javascripts
│ ├── images
└── test/
...
There are two things that needs to be added to the application before it can run. First, you must have the latest version of the RESOLVE compiler. You can obtain this by running the maven install command on the compiler project. Place the generated jar
file inside the custom_lib
folder. Note that there is already a version inside test/lib
folder. Do not use this version! This version is only used for integration and unit testing. There is no guarantee that it will produce the same results as the latest version of the compiler.
In addition to the RESOLVE compiler, you will need to supply a RESOLVE workspace folder containing all the library files for the RESOLVE
language. The workspace can be found here. Note that you can have multiple distinct copies of the RESOLVE workspace folder (with different names).
Lastly, you will need to use the local-config-template.conf
and create a local-config.conf
file with all the required information filled in. This contains information on the various port numbers as well as a path to all the RESOLVE workspaces.
The creation and continual evolution of the RESOLVE language is owed to an ongoing joint effort between Clemson University, The Ohio State University, and countless educators and researchers from a variety of other institutions.
Developers of this particular test/working-iteration of the RESOLVE WebAPI
include:
- RESOLVE Software Research Group (RSRG) - School of Computing, Clemson University
Copyright © 2020, RESOLVE Software Research Group (RSRG). All rights reserved. The use and distribution terms for this software are covered by the BSD 3-clause license which can be found in the file LICENSE.txt
at the root of this repository. By using this software in any fashion, you are agreeing to be bound by the terms of this license. You must not remove this notice, or any other, from this software.