KIV: Quick Start
General
We assume that you have downloaded and installed the KIV Eclipse plugin already.
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 
.
In the left pane at the top is the KIV Navigator, which displays KIV projects. The screenshot shows a project separation. Projects consist of specifications and theorem files sequents 
, which come in pairs. In the middle you can see the editor displaying a specification text. You can use the icon 
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.
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. 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:
- It tracks a list of previously used locations
- It shows a list of projects that are siblings to the selected location. This is useful if you want to import multiple projects at once.
Deleting a KIV project is straight-forward. If you choose to delete the existing files, two things can happen
- If the project files reside in the workspace, the project will actually be deleted.
- Otherwise, if the project was linked to a different location, this will only delete the Eclipse files of the project, not the KIV files. Hence, you can re-import it later.
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 specifications 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
- Install resp. Reload: parse and load the specification to the internal representation.
- Edit: open the specification file in the Eclipse Editor
- Edit Sequents: open the sequents file in the Eclipse Editor
- View/View Signature: Display what KIV currently maintains as the specification's text (Hint: Project → Check Specifications detects inconsistencies)
- Work On: start defining and proving lemmas
Institute for Software & Systems Engineering
The Institute for Software & Systems Engineering (ISSE), directed by Prof. Dr. Wolfgang Reif, is a scientific institution within the Faculty of Applied Computer Science of the University of Augsburg. In research, the institute supports both fundamental and application-oriented research in all areas of software and systems engineering. In teaching, the institute facilitates the further development of the faculty's and university's relevant course offerings.