CorC

With CorC, we implemented an IDE to create programs following the Correctness-by-Construction approach. Starting with an abstract specification, CorC supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinements.

16
mentions
5
contributors

What CorC can do for you

CorC

Correctness-by-Construction (CbC) is an approach to incrementally create correct programs. Guided by pre-/postcondition specications, a program is created using refinement rules, guaranteeing the resulting implementation is correct. With the Eclipse plugin CorC, we implemented a graphical and textual IDE to create programs following the CbC approach. Starting with an abstract specification, CorC supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinement steps using a theorem prover.

WebCorC

With WebCorC, we offer a basic version of CorC in the web without the need to set up Eclipse.

C-CorC

CorC for information flow (C-CorC) is an extension of CorC.

Getting Started

CorC requires Eclipse Modelling Tools (EMT) to be installed and extended with various plugins.

Java Version

Install JDK 16. CorC may not work out of the box with newer versions.

Software

  • Install Eclipse Modelling Tools (Version 2023-09).
  • Get the latest release of Z3 and add the */z3-[cur-version]-[x64/x32]-win/bin folder to the environment variable PATH

EMT Plugins

CorC Setup

  1. Clone the repo:

    git clone https://github.com/KIT-TVA/CorC.git
    
  2. Install JaMoPP using the two plugins inside package *.tool.update (disable Group items to show available plugins).

  3. Open the following packages in Eclipse Modelling Tools:

    • de.tu-bs.cs.isf.cbc.exceptions
    • de.tu-bs.cs.isf.cbc.model
    • de.tu-bs.cs.isf.cbc.mutation
    • de.tu-bs.cs.isf.cbc.tool
    • de.tu-bs.cs.isf.cbc.util
    • de.tu-bs.cs.isf.cbcclass.tool
    • de.tu-bs.cs.isf.wizards
    • de.tu_bs.cs.isf.cbc.parser
    • de.tu_bs.cs.isf.cbc.statistics
    • de.tu_bs.cs.isf.cbc.statistics.ui
    • de.tu_bs.cs.isf.commands.toolbar
    • de.tu_bs.cs.isf.lattice
  4. Open:

    • *.cbc.model -> model -> genmodel.genmodel
    • *.cbc.statistics -> model -> cbcstatistics.genmodel

    Right click and Generate Model/Edit/Editor Code for all files listed.

  5. Select any package and run project as Eclipse Application.

Examples & Case Study Introduction

We provide different examples and case studies to explore CorC!

Examples

Create CorC-examples via File -> New -> Other... -> CorC -> CorC Examples Select examples you want to create.

Case studies

The repository you checked out contains various software product line case studies. They can be loaded via File -> Open project from file system.

BankAccount

The BankAccount implements basic functions of a bank account such as withdrawals, limits, money transfers and checking the account balance.

  • BankAccount Object-oriented implementation with class structure and CbC-Classes.
  • BankAccountOO Object-oriented implementation with class structure and CbC-Classes. Non-SPL implementation.

Elevator

The Elevator implements basic functions of an elevator such as the movement and entering and leaving of persons.

  • Elevator Object-oriented implementation with class structure and CbC-Classes.

Email

The product line Email implements basic functions of an email system including server- and client-side interactions.

  • EmailOO Object-oriented implementation with class structure and CbC-Classes. Non-SPL implementation.
  • EmailFeatureInteraction Java-Implementation without implementation with CbC.

IntegerList

The IntegerList implements a list of integers with add and sort operations.

  • IntegerList Object-oriented implementation with class structure and CbC-Classes.
  • IntegerListOO Object-oriented implementation with class structure and CbC-Classes. Non-SPL implementation.

Common Issues

Problem: EMT gets stuck while trying to generate a model.

Solution: Terminate EMT using any process manager and generate the model again.


Problem: Multiple resolving errors after generating model files.

Solution: Uninstall JaMoPP Plugins via Window -> Preferences -> Install/Update -> Uninstall or update. Afterwards reinstall as described above.


Problem: Cycling depedency issues.

Solution: Navigate to: Project -> Properties -> Java Compiler -> Building -> Configure Workspace Settings -> Build path problems -> Circular dependencies and set the listbox to Warning.


Problem: Errors in certain files about undefined methods and classes.

Solution: Changing the compliance: Project -> Java Compiler -> JDK Complicance -> Use compliance from execution environment 'JavaSE-16'.

Logo of CorC
Keywords
Programming languages
  • Java 98%
  • GAP 1%
License
Not specified
</>Source code

Participating organisations

Karlsruhe Institute of Technology (KIT)
Technische Universität Braunschweig

Reference papers

Mentions

Contributors

MK
Maximilian Kodetzki
Karlsruhe Institute of Technology (KIT)
TB
Tabea Bordis
FD
Fynn Demmler
TU Braunschweig
IS
Ina Schaefer

Related projects

no image

Core Informatics

A Helmholtz Pilot Program

Updated 13 months ago
In progress