ISSE

Search

KIV: Quick Start

This is a small tutorial on the new Scala Version of KIV. We assume that you have downloaded and installed the KIV Eclipse plugin already.

The Documentation covers the logic and specification language of KIV in greater detail.

Main Page

General

The KIV plugin comes with its own perspective that is shown in the screenshot. The perspective can be activated via Window -> Open Perspective -> Other or by clicking on the button KIV.

In the left pane at the top is the KIV Navigator, which displays KIV projects. The screenshot shows a project tree-flatten. Projects consist of specifications specification and theorem files sequents sequents, which come in pairs.

In the middle you can see the editor displaying a specification text. You can use the icon toggle to switch between a specification and its theorem file.

At the bottom in the left pane you find the symbol table, which shows available mathematical symbols. You can click on a symbol to insert it into the editor at the cursor. Alternatively, you can type a backslash \ to open an autocomplete form for mathematical symbols.

The editor provides a presentation parser that detects syntax errors as you type. Note that KIV specifications are encoded with UTF-8.

KIV Perspective

Create/Import Projects

Each project contains several files that are specific to Eclipse (e.g., .project) and other files that are required by KIV (e.g., devgraph).

To create a new project, right-click into the navigator, select New -> KIV project and follow the instructions.

KIV Perspective

You will be prompted to insert a project name, and optionally a custom location. Similar to Java projects, the actual files of a KIV project need not to reside in the workspace folder themselves. If you specify a custom location that is not at the top-level of the workspace, KIV will create the new project there and just link the files into the workspace. Please keep this in mind when you back up your workspace!

You can import an existing KIV project similarly. Note that the import currently does not copy projects. The import dialog has several features:

Deleting a KIV project is straight-forward. If you choose to delete the existing files, two things can happen

Development Graph

Running KIV on a project

Right-click on a project in the navigator and select Open Project in KIV to start the interactive proof environment. It will show the development graph of the project, consisting of a hierarchy of specifications.

Orange nodes are imported from the library. Blue and green nodes represent specifications contained in the project. The color green indicates that the specification is in "Proved State", i.e., all theorems have been proven and all dependencies are checked.

For more information, see the Tour.

Specification/Proof Cycle

In a new project you start with an empty development graph. You can import specifciations from existing (library-) projects (Menu: Project), and you can create new specifications (Menu: Specification).

A right-click on a node in the graph opens a menu