CbC is an approach to create correct programs incrementally. Guided by pre-/postcondition specifications, a program is developed using refinement rules, guaranteeing the implementation is correct. With 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 deductive verifier.

Learn more about CorC and the underlying concepts in the wiki.

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

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

• Graphiti Install Graphiti using the update site https://download.eclipse.org/graphiti/updates/release/0.18.0

• FeatureIDE Available in Eclipse Marketplace

• Mylyn Available in Eclipse Marketplace (Mylyn 3.23)

• TestNG Available in Eclipse Marketplace

1. Clone the repo:

   git clone https://github.com/KIT-TVA/CorC.git

2. In EMT, select Open Projects... -> CorC and check the boxes for the following packages:

   • 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
   • de.tu_bs.cs.isf.proofrepository
   • de.kit.tva.lost

3. Open:

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

   Right click and Generate Model/Edit/Editor Code for all files listed. If EMT still displays errors, clean and rebuild all projects as described in the common issues section.

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

1. Create a fork.
2. Create a new branch with a name that describes your new feature.
3. Ensure that the command mvn compile spotless:apply runs successfully.
4. Start a pull request.

We use the default Eclipse formatting style with spotless. Run mvn spotless:apply to format all src files automatically if needed.

We provide different examples and case studies to explore CorC!

Create CorC-examples via File -> New -> Other... -> CorC -> CorC Examples.

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

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.

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.

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.

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.

Problem: Multiple errors resulting from forbidden references or undefined types.

Solution: In Eclipse Modelling Tools:

1. Preferences -> Java -> Compiler -> Errors/Warnings -> Deprecated and restricted API: Set Forbidden References to ‘Warning’.
2. Preferences -> Java -> Installed JREs: Select the correct JDK21 folder on your system and set the checkmark.
3. Preferences -> Java -> Installed JREs -> Execution Environment: Select JavaSE-21 and check the ‚jre [perfect match]‘ box.
4. Clean and rebuild all projects via Project -> Clean....

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: Clean and rebuild all projects via Project -> Clean....

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'.

Problem: Errors involving the message 'Cannot modify resource set without a write transaction'.

Solution: Delete the folder .settings in org.eclipse.core.runtime within the current workspace. If that doesn't resolve the issue, delete all .settings folders and the .project file in the CorC folder.

Problem: Some library file or package that is in the git is not shown locally in eclipse and there are errors missing that file

Solution: Press F5 when hovering over the parent directory of the missing file. The file should appear.