Skip to content

Home

Jump to bottom
Fynn Demmler edited this page Jan 31, 2025 · 29 revisions

CorC Ecosystem: What it is and why it matters

Functional correctness is a central aspect of every software system. Software development approaches based on test cases are a fast and reliable way to show that the tested parts of a software system function as intended. However, the test case's main advantage—partial guarantees—is also its biggest drawback. Comprehensive functional correctness guarantees are required in many software systems, and verification is used to ensure that.

Correctness-By-Construction (CbC) engineering introduced by Kourie and Watson is based on Design-by-Contract, which connects contracts with programs. Using logical formulas, a program's contract formally specifies what it expects as input, the precondition, and which outputs it produces, the postcondition. Traditionally, once a program is implemented and specified, it is verified afterwards whether it fulfills its obligations according to its contract. This approach is called post-hoc verification. The main idea behind CbC is to guide developers in incrementally specifying and implementing a program. Stepwise specification and implementation enable the creation of correct programs by construction since each specification and implementation step can be verified through deductive verifiers. This is the key advantage of CbC compared to post-hoc verification. Implementing a program using CbC starts with an abstract hoare triple {P}S{Q} where symbols P and Q are the pre- and postcondition of the program, and symbol S represents the implementation abstractly. Given a set of refinement rules, we can refine the symbol S iteratively to concrete code. Each refinement rule has side conditions that we must specify.

CorC currently contains a plethora of extensions. We call CorC, including all of its extensions, the CorC ecosystem.

CbC Example

Since the introduction is somewhat abstract, we examine how CbC works in a simple example. We want to create a program that returns TRUE, iff some natural number n is even, else it returns FALSE. We will store the return value in a boolean variable ret. Given the abstract hoare triple

{P} S {Q}

we define pre condition P := n > 0. That is, we require the number n to be bigger than 0, which must be ensured by the callee. Consequently, the program must ensure the following postcondition Q := (n % 2 == 0 -> ret = TRUE) & (n % 2 != 0 -> ret = FALSE) after execution. We now decide to use the selection refinement rule, which is similar to branching in Java to refine the abstract hoare triple into a new refinement:

{P} S {Q} 
⊑ {P} if G1 -> S1 elseif G2 -> S2 {Q}

As we can see, there are some new conditions G1, G2, called guards, and abstract statements S1, S2. Guards G1 and G2 are the required side conditions for the selection refinement for our example. As we will see, statements S1 and S2 can be further refined separately. Since we want to differentiate between the number n being even n % 2 = 0 and uneven n % 2 != 0, we use these as guards G1 := n % 2 = 0 and G2 := n % 2 != 0.

Lastly, we need to refine statements S1 and S2. We use the statement refinement rule for both:

{P} S {Q} 
⊑ {P} if G1 -> S1 elseif G2 -> S2 {Q}
⊑ {P} if G1 -> TRUE elseif G2 -> S2 {Q}
⊑ {P} if G1 -> TRUE elseif G2 -> FALSE {Q}

with

P := n > 0
Q := (n % 2 = 0 -> ret = TRUE) & (n % 2 != 0 -> ret = FALSE)
G1 := n % 2 = 0
G2 := n % 2 != 0

We have created a fully specified CbC program that can be verified with a deductive verifier like KeY. One of the main benefits of this approach compared to post-hoc verification is that we can also verify every refinement step independently, which is challenging with post-hoc verification.

CbC Refinement Rules

Following is a list of all existing CbC refinement rules:

  • Skip | {P} skip {Q} iff P implies Q
  • Assignment | {P} x := E {Q} iff P implies Q[x\E]
  • Composition | {P} S1 ; S2 {Q} iff there is an intermediate condition M such that {P} S1 {M} and {M} S2 {Q}
  • Selection | {P} if G1 → S1 elseif . . . Gn → Sn fi {Q} iff (P implies G1 ∨ G2 ∨ . . . ∨ Gn) and {P ∧ Gi} Si {Q} holds for all i.
  • Repetition | {P} do [I, V] G → S od {Q} iff (P implies I) and (I ∧ ¬G implies Q) and {I ∧ G ∧ V=V0} S {I ∧ 0≤V ∧ V < V0} and {I ∧ G} S {I}
  • Method Call | {P} b := m(a1, ..., an) {Q} with method {P′} return r m(param p1, ..., pn) {Q′} iff P implies P′[pi\ai] and Q′[poldi \ aoldi , r\b] implies Q

CorC Refinement Rules

CorC's refinement rules build a superset of CbC's refinement rules. Additional refinement rules are:

  • Original Call | Call the method with the same signature from the parent feature in a SPL.
  • Return Assignment | Automatically sets the return variable ret to the expression returned inside this assignment.

CorC Example

Let us consider the program from the CbC Example section. We want to implement that program in CorC.

  1. Create a new Java Project: File -> New -> Project... -> Java Project.
  2. Create a folder named isEven inside the folder src.
  3. Create a new CorC diagram: Right-click -> New -> Other... -> new CorC File. We name it isEven:
  4. Now we start creating the CbC program. We introduced the Formula f including it's pre- and postcondition and the variables boolean ret and int n inside the Variables block using drag-and-drop from the Palette.
  5. We now introduce a SelectionStatement s and add another guard by drag-and-dropping an ExtraSelection onto the selection s. We also connect the abstract hoare triple f with selection s using the Refinement connection.
  6. Finally, we add two return assignments ReturnStatement and connect them to the selection s.
  7. We now verify the entire CbC program or each refinement rule separately through the context menu.
  8. To convert the method isEven into Java code, we click Generate Code in the context menu. ]

Project Types

CorC currently supports three different project types: Non-object-oriented projects, object-oriented projects, and software product lines.

Non-object Oriented Projects

A non-object-oriented project contains not classes but a finite number of CbC methods. This project type helps create small programs.

  1. Create a new Java project.
  2. Create a folder named src.
  3. Handle any CbC program inside the src folder.

Object-Oriented Projects

Object-oriented projects are based on CbC classes and CbC methods. We may create a CbC class diagram via the file wizard. Upon creation we'll find a new .cbcclass file in the project. CbC class diagrams essentially depict a high-level view of the class, its fields, and methods. CbC class diagrams are internally linked to their respective CbC method diagrams, identified through the .cbcdiagram file type, so any variable changes are automatically adjusted in the CbC classes and CbC methods. CbC classes must reside in a folder with the same name. CbC methods reside in the same folder as their respective class.

  1. Create a new Java project.
  2. Create a folder named src.
  3. Create a folder with the name of some class A inside src.
  4. Create a CbC class named A inside folder A.
  5. Insert CbC methods belonging to class A in folder A. (TODO: Example here.)

Software Product Lines

We may implement software product lines (SPL) in CorC. The project structure for SPLs requires additional information about their features and underlying feature model, which is given through a model description file.

  1. Create a new Java project.
  2. Create a folder named src.
  3. Define a model description file model.xml and place it inside the java project.
  4. Create one folder for every feature in the model and place them inside folder src.
  5. Place any CbC classes and methods inside their respective feature folder according to the principles of object-oriented projects.

Extensions

The CorC ecosystem provides a plethora of extensions. We now list the most commonly used extensions. Most extensions not listed here are accessible through the context menu in CorC.

Graphical Editor

The graphical editor provides diagram elements to create CbC programs graphically.

  • The white canvas contains the content of a CbC program, which in this case is called graphical_editor.
  • The Palette contains all tools to manipulate the diagram, including all CorC refinements.
  • The window tabs on the bottom are called Eclipse property views. These can be opened and closed on demand through Window -> Show View -> Other....

Textual Editor

In addition to the graphical editor, we provide a textual editor called LOST-Editor. The LOST-Editor is based on the LOST DSL and is accessible through the Eclipse property view (Window -> Show View -> LOST-Editor). In LOST, each line represents an operation or is part of Java code. A line followed by a tab indicates a new refinement. With this, we get a tree-like code structure in which the number of tabs represents the depth of the tree of a CorC diagram before each refinement. Developers specify refinements sequentially, starting from the abstract hoare triple and continuing through its refinements sequentially. LOST supports the same refinement rules as the graphical editor:

  • F(pre: [preCondition], post: [postCondition]) - Formula with pre- and post-condition.
  • C(intm: [intermediateCondition]) - Composition with its intermediate condition.
  • S(guard: [guard1], guard: [guard2], ...) - Selection statement and its guards.
  • L(inv: [invariant], guard: [guard], var: [variant]) - Repetition statement ("Loop") and its invariant, guard, and variant.
  • [statement] ; - Basic statement.
  • O: [statement] ; - Original statement. Used in SPLs to refer to the definition of the parent of any given method.
  • R: [statement] ; - Return statement.
  • M: [statement] ; - Method call statement.
  • skip - Skip statement.
  • { [statements] } - Block of Java code.

Additionally, each refinement rule supports the specification of modifiables variables. Specify the initializer mod: [modifiable] as the first parameter of any refinement rule, e.g., F(mod: x, pre: x > 0, post: y > 0). Further details are described in the LOST-documentation.

Verification

Verifying entire CbC programs and single refinement rules in CorC is possible through the deductive verifier KeY. There are two ways to verify CbC programs in CorC. Through the graphical editor and the textual editor. The verification process is identical for both extensions. Once the verification process is started, CorC generates proof obligations for KeY in .key files found in the current project folder. Every time KeY provides output, CorC shows status information depending on the response from KeY. Afterward, the verification results are saved in .proof files next to their corresponding .key files. All successfully verified refinements are highlighted in green in the graphical editor if the verification was successful. If the proof for a refinement rule is not closeable, CorC will highlight the refinement in red.

Verification in the Graphical Editor

  • Open the console property view through Window -> Show View -> Console to monitor the verification process.

Verifying all refinements:

  1. Right-click anywhere in a CbC diagram.
  2. Select Verify -> Verify All Statements.

Verifying single refinements:

  1. Right-click on any refinement.
  2. Select Verify -> Verify a statement.

Verification in the Textual Editor

  1. Open the console property view through Window -> Show View -> Console to monitor the verification process.
  2. Open the LOST-editor.
  3. Press the button Load.
  4. Press the button Verify.

Proof Statistics

Statistics like execution time, proof status, number of branches, and more can be summarized and visualized with the proof statistic extension. To show proof statistics for a single CbC program: Right-click the diagram -> View CorC Statistics. Furthermore, CorC provides diagrams for the average execution time and the time per configuration in SPLs if multiple CbC programs are selected. These diagrams are shown at the bottom of the Statistics Viewer. Note that the diagrams are generated by R. Therefore, we must install and add it to the environment variable PATH to view proof statistic diagrams.

Counterexample Generation

Our counterexample generation extension is another valuable tool for finding bugs in CbC programs. CorC uses Z3 to generate counterexamples for non-closeable proofs. To enable the generation of counterexamples: View: Properties -> Settings -> Generate Counterexamples. Once we activate this option, CorC provides a counterexample for every non-closeable proof, if possible. Note that Z3 uses special syntax to represent counterexamples. Their wiki provides more information.

Test Case Generation

The CorC ecosystem includes a test generation extension that generates test cases for single refinements of CbC programs. Depending on the program's complexity, we may provide custom input values for the supported data types through the Testing tab in the Eclipse property view. The extension also supports automatic input generation, either by use of default values for data types or through SMT solving with the Z3 SMT-solver. After the generation of test cases, the extension uses TestNG to execute those test cases. Successfully tested refinements will be highlighted in orange in the graphical editor. Furthermore, the console outputs testing status information. If a test case fails, the console will provide the user with detailed error information, and the corresponding refinement will be changed to red in the graphical editor. This extension is also available in the LOST-Editor. Test one or more refinements in the graphical editor by:

  1. Configure the test case generation extension through the Properties -> Testing tab.
  2. Right-click a refinement or anywhere else in a CbC method diagram.
  3. Select Test and a suitable testing option.
  4. (Optional) Navigate to the Console tab to view status information during and after testing.

Mutation Generation

The mutation feature allows the mutation of refinements that contain Java code with MuJava. Furthermore, mutating conditions via a separate mutation module that does not use MuJava is possible. Every mutant is generated as a new CbC program and can be found inside the mutations folder inside the project. Resulting CbC programs are not guaranteed to be correct according to their specification.

Code Mutation

To mutate any applicable refinement rule inside CorC, proceed as follows:

  1. Select the refinement rule.
  2. Navigate to the 'Mutations' in the properties window.
  3. Select the desired mutation operators and press the mutate button.

Code Mutation Example

Suppose the statement i = i + 1; is part of a CbC program in CorC. Some possible mutations for this statement are:

  • i = i - 1;
  • i = i * 1;
  • i = i / 1;
  • i = i % 1;

Condition Mutation

To mutate conditions follow:

  1. Select a condition.
  2. Navigate to the 'Mutations' in the properties window.
  3. Select the desired mutation operators and press the mutate button.

Condition Mutation Example

Given the condition i > 0 -> TRUE, some possible mutations are the following

  • i >= 0 -> TRUE
  • i < 0 -> TRUE
  • i == 0 -> TRUE
  • i != 0 -> TRUE

Code to CbC

Use the Code to CbC extension to generate a CbC program from plain Java code. The extension generates the corresponding diagram in the graphical editor. Following the creation of the diagram, we must provide missing conditions for the refinement rules. Use the extension by:

  1. Select the Java source file.
  2. Press the context menu option Generate Diagrams from Class.
  3. Add additional conditions to the generated Java code using JML.

Information Flow

The CorC ecosystem supports the definition of information flow policies and provides an extension to create programs that comply to these policies by construction.

To use the information flow functionally, you can create new secure variables by adding Variables and Variable from the Palette, and using these variables in the program. For example, a private variable x can be introduced by writing private in the Confidentiality column.

ArchiCorC

ArchiCorC is a separate software system that interfaces with CorC for Component-based software engineering with CbC.

CbC/CorC-Related Papers

  • M. Kodetzki, T. Bordis, T. Runge, and I. Schaefer. Partial Proofs to Optimize Deductive Verification of Feature-Oriented Software Product Lines. In 18th International Working Conference on Variability Modelling of Software-Intensive Systems (VaMoS'24), 2024.
  • T. Runge, T. Bordis, A. Potanin, T. Thüm, and I. Schaefer. Flexible Correct-by-Construction Programming. In Logical Methods in Computer Science, Volume 19, 2023.
  • T. Runge, Correctness-by-Construction for Correct and Secure Software Systems. Dissertation, 2023.
  • T. Runge, M.erveto, A. Potanin, and I. Schaefer. Immutability and Encapsulation for Sound OO Information Flow Control. In ACM Transactions on Programming Languages and Systems, Volume 45, 2023.
  • T. Runge, A. Potanin, T. Thüm, and I. Schaefer. Traits for Correct-by-Construction Programming. In CoRR 2022.
  • T. Bordis, T. Runge, D. Schultz, and I.Schaefer. Family-Based and Product-Based Development of Correct-by-Construction Software Product Lines. In Journal of Computer Languages #COLA), 2022.
  • T. Bordis, L. Cleophas, A. Kittelmann, T. Runge, I. Schaefer, and B. W. Watson. Re-CorC-ing KeY: Correct-by-Construction Software Development Based on KeY. In The Logic of Software. A Tasting Menu of Formal Methods, 2022.
  • T. Runge, A. Potanin, T. Thüm, and I. Schaefer. Traits: Correctness-by-Construction for Free. In FCRTE 2022.
  • A. Kittelmann, T. Runge, T. Bordis, and I. Schaefer. Runtime Verification of Correct-by-Construction arriving Maneuvers. ISoLA 2022.
  • T. Bordis, M. Kodetzki, T. Runge, and I. Schaefer. VarCorC: Developing Object-Oriented Software Product Lines Using Correctness-by-Construction. In SEFM Workshops, 2022.
  • T. Runge, A. Kittelmann, M. Servetto, A. Potanin, and I. Schaefer. Information Flow Control-by-Construction for an Object-Oriented Language. SEFM 2022.
  • I. Schaefer, T. Runge, L. Cleophas, and B. W. Watson. Tutorial: The Correctness-by-Construction Approach to Programming Using CorC. SecDev, 2021.
  • T. Runge, T. Bordis, T. Thüm, and I. Schaefer. Teaching Correctness-by-Construction and Post-hoc Verification - The Online Experience. FMTea, 2021.
  • T. Bordis, T. Runge, and I. Schaefer. Correctness-by-Construction for Feature-Oriented Software Product Lines. In GPCE, 2020.
  • T. Runge, A. Knüppel, T. Thüm, and I. Schaefer. Lattice-Based Information Flow Control-by-Construction for Security-by-Design. In FormaliSE, 2020.
  • A. Knüppel, T. Runge, and I. Schaefer. Scaling Correctness-by-Construction. ISoLA, 2020.
  • T. Bordis, T. Runge, A. Knüppel, T. Thüm, and I. Schaefer. Variational Correctness-by-Construction. In 14th International Working Conference on Variability Modelling of Software-Intensive Systems (VaMoS'20e, 2020.
  • T. Runge, T. Thüm, L. Cleophas, I. Schaefer, and B. W. Watson: Comparing Correctness-by-Construction with Post-Hoc Verification - A Qualitative User Study. In REFINE, 2019.
  • T. Runge, I. Schaefer, L. Cleophas, T. Thüm, D. G. Kourie, and B. W. Watson: Tool Support for Correctness-by-Construction, Proc. of the International Conference on Fundamental Approaches to Software Engineering (FASE), Springer, 2019.
  • T. Runge, I. Schaefer, A. Knüppel, L. Cleophas, D. G. Kourie, and B. W. Watson: Tool support for Confidentiality by Construction. In HILT 2018 Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems (HILT'18), 2018.
  • I. Schaefer, T. Runge, A. Knüppel, L. Cleophas, D. G. Kourie, and B. W. Watson: Towards Confidentiality-by-Construction. In International Symposium on Leveraging Applications of Formal Methods, Springer, 2018.

References

  • Kourie, Derrick G., and Bruce W. Watson. The Correctness-by-Construction Approach to Programming. Vol. 264. Heidelberg: Springer, 2012.
  • Meyer, Bertrand. Applying Design by Contract. Computer 25.10 (1992): 40-51.
  • Watson, Bruce W., et al. Correctness-by-construction and post-hoc verification: a marriage of convenience?. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I 7. Springer International Publishing, 2016.
  • Bordis, Tabea, et al. Family-based and product-based development of correct-by-construction software product lines. Journal of Computer Languages 70 (2022): 101119.
Clone this wiki locally