BeginToReason2
is a tutor that utilizes the RESOLVE programming language to pinpoint difficulties and help CS students as they learn how to rigorously trace the code they encounter. This version is a transformation to a tutor and it features a new back-end build using Python and Django and a front-end that incorporates Bootstrap and communicates with the RESOLVE verification engine.
A long term goal of BeginToReason2
is to be a Reactive, RESTful API.
RESOLVE (REusable SOftware Language with VErification) is a programming and specification 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.
- Clone this repository:
git clone https://github.com/ClemsonRSRG/beginToReason2.git
- In the root application folder, use the command listed below with either
dev-requirements.txt
(development + production) orrequirements.txt
(production only) to install the necessary dependencies.pip install -r <name of requirements>.txt
- Note:
dev-requirements.txt
also installs the dependencies inrequirements.txt
, so no need to run both commands.
- Apply database migrations:
python manage.py migrate
- To run the application:
python manage.py runserver
- Note 1: This will use the default development settings in the repository. For production environments, please consult Django Deployment Documentation.
- Note 2: By default, your application will be running on port
8000
. Please consult theurls.py
file underbegintoreason_django
(and the sub-applications'urls.py
) for all links that can be visited in this application.
For any additional instructions on how to run a Django application, please consult the Django Documentation.
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 BeginToReason2
include:
- RESOLVE Software Research Group (RSRG) - School of Computing, Clemson University
- Florida Atlantic University
- Rose-Hulman Institute of Technology
Copyright © 2021, 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.