# CAPSDoc

## Table of Contents

## 1 What is CAPS?

CAPS is a system for the derivation of imperative programs from formal specifications. The system provides a tactic based framework for carrying out program as well as formula transformations in a coherent way. It automates the mundane formula manipulation tasks by employing automated theorem provers.

## 2 Derivation Methodology

While developing program in CAPS, at every stage, there is always a correct-by-construction partial program with some unknown subprograms, as shown in the example in Figure 1.

Figure 1: Sketch of an example derivation (maximum segment sum problem)

All program constructs in the system, including the unknown subprograms have associated pre- and post-conditions. Program constructs are introduced only when logical manipulations show them to be sufficient for maintaining the correctness. For example, in Figure 1(c), variable \(r\) needs to be modified in the loop body to maintain the loop invariant \(P_0\) . The required update for \(r\) naturally follows from the simplification of the correctness proof obligations. An important feature of our system is that a user cannot construct an incorrect program in it. Apart from the fully annotated derived program, the system also maintains the derivation tree which reproduces the complete derivation process and provides opportunities for exploring the alternative solutions by backtracking and branching.

## 3 Related Publications

**Theoretical foundations**

- Assumption Propagation Through Annotated Programs - Dipak L. Chaudhari and Om P. Damani. Formal Aspects of Computing, in press.
- Automated Theorem Prover Assisted Program Calculations - Dipak L. Chaudhari and Om P. Damani. The 11th International Conference on Integrated Formal Methods, IFM 2014.
- Combining Top-down and Bottom-up Techniques in Program Derivation - Dipak L. Chaudhari and Om Damani. 25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015.

**System building aspect**

- Building an IDE for the Calculational Derivation of Imperative Programs - Dipak L. Chaudhari and Om P. Damani. Second Workshop on Formal-IDE, F-IDE 2015.

**Educational Usage**

- Introducing Formal Methods via Program Derivation - Dipak L. Chaudhari and Om P. Damani. 20th Annual Conference on Innovation and Technology in Computer Science Education, ITiCSE 2015.

## 4 Installation

### 4.1 Prerequisites

#### 4.1.1 System Requirements

- Linux
- Google Chrome Browser

#### 4.1.2 Prerequisites

- Java Runtime Environment
- Why3 verification framework (v0.81)
As a part of the Why3 installation, you will also need to install the external provers. Following external provers are supported in CAPS.

- Z3
- Alt-Ergo
- CVC3
- SPASS

At least one of these theorem provers needs to be installed. We recommend **Z3** since CAPS can also connect to **Z3** directly.

#### 4.1.3 Why3 Installation

The following instructions should work. In case of problems, please refer detailed installation instructions at the Why3 homepage (http://why3.lri.fr/).

- Install Ocaml and libraries
http://why3.lri.fr/doc-0.81/manual006.html#sec38

sudo apt-get install ocaml ocaml-native-compilers sudo apt-get install liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev libocamlgraph-ocaml-dev

- Install Why3
wget https://gforge.inria.fr/frs/download.php/file/33491/why3-0.81.tar.gz tar -xzf why3-0.81.tar.gz cd why3-0.81/ ./configure

Make sure that the "configure" is successful. Sample configure summary below.

Summary ----------------------------------------- Verbose make : no OCaml compiler : yes Version : 3.12.1 Library path : /usr/lib/ocaml Native compilation : yes Profiling : no IDE : yes Bench tool : no Documentation : no Coq support : no (coqc not found) PVS support : no (pvs not found) Frama-C support : no Hypothesis selection : yes Installable : yes Binary path : ${exec_prefix}/bin Data path : ${prefix}/share/why3 Relocatable : no

Proceed with the installation.

make sudo make install cd ..

#### 4.1.4 Z3 Installation

Download Z3 v4.3.1 source: Z3 v4.3.1 Source

sudo apt-get install python autoconf unzip z3-89c1785b73225a1b363c0e485f854613121b70a7.zip -d z3 cd z3 autoconf ./configure python scripts/mk_make.py cd build make sudo make install

#### 4.1.5 Configure Why3 to detect provers

Run the following command to to detect freshly installed provers.

why3config --detect-provers

### 4.2 CAPS Installation

The latest version of the CAPS can be downloaded here.

Extract the archive. It contains the following files.

application.conf # Sample config file staged/ start # start script

Update the Why3 path and other variables in the `application.conf`

file.

Run the start command to start the server

chmod u+x ./start ./start -Dconfig.file=./application.conf

Connect to http://localhost:9000 to access the CAPS application GUI. Login with user name `user1@company.com`

and passsword `secret1`

.

## 5 Usage

(The videos are for the older version. The tactic names and parameters might not match.)

### 5.1 Starting the derivation

Start the derivation by applying the `Init4` tactic.

### 5.2 Steps for deriving "If" program constructs

There two ways of deriving if program construct

#### 5.2.1 IfIntro

You can directly introduce an If program construct by directly providing the guards of the If Program (`IfIntro`

tactic).

#### 5.2.2 StepIntoBA and StepIntoIFBA

- Start the derivation by applying the
`StepIntoBA`

tactic on an`UnknownProgram`

node. You will need to specify the variables that occur on the left hand side of the assignments in the body of the`if`

. For example, if there are three variables`x`

,`y`

, and`z`

but you don't intend to make any assignment to`z`

, then can you can just specify variables`x`

and`y`

- Once in the formula mode, you can instantiate meta variables by applying the
`InstantiateMeta`

tactic and guess the guards by applying the`GuessGuard`

tactic. On stepping out from the formula mode, an`IfProgram`

is constructed form the guessed guards and instantiated meta variables. - To derive additional guards, apply the
`StepIntoIFBA`

tactic to the`IF`

program.

### 5.3 Propagating Assumptions

### 5.4 Stepping into subprograms

To step into a subformula, apply the `StepIntoProgId` tactic.

### 5.5 Stepping into subformulas

To step into a subformula, apply the `StepIntoSubFormula` tactic.

### 5.6 SimplifyAuto tactic

To simplify the current formula with the help of ATPS, apply `SimplifyAuto` tactic.

### 5.7 Input commands for logical operators

|-----------------------+---------------| | operator | Input command | |-----------------------+---------------| | Conjunction | \and | | Disjunction | \or | | Negation | \neg | | Equivalence | \equiv | | Implication | \implies | | Universal Quantifier | \forall | | Existential Quantifer | \exists | |-----------------------+---------------|

### 5.8 Input commands for arithmetic operators

|----------------+---------------| | operator | Input command | |----------------+---------------| | Addition | + | | Subtraction | - | | Multiplication | \ast | | Division | \slash | |----------------+---------------|

## 6 Troubleshooting

### 6.1 I am getting `TacticInputParseError(Failed to parse the tactic)`

error

- Formulas like 0 ≤ i < N are not supported. Type them as 0 ≤ i \and i < N
- Ensure that you have specified type for all the variables

### 6.2 `IntroAssignmentTactic`

fails : `Proof obligation for the assignment can not be discharged`

- Ensure that the external theorem provers are configured properly.

## 7 Source

Source is available at https://github.com/dipakc/CAPS

Derivation examples: DerivationExamples