A tool for proving inductive properties of software systems specified with constructor-based logics
The Constructor-based Inductive Theorem Prover (CITP) is a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features.
The tool consists of two parts:
CITP is implemented in Core Maude.
CITP consists of only one file, citp.maude (now at version 2.0). However, please note that you need to have Maude installed in order to use the tool.
Alternatively, you can obtain the full CITP distribution (including a set of example specifications and proofs) from its GitHub repository by using:
git clone https://github.com/ittutu/CITP.gitTo use CITP, simply copy the file citp.maude to your current/working directory, open a terminal, and type:
maude citp.maudeIf you are using the GitHub distribution, it suffices to open a terminal to the CITP directory and to type:
maude Tool/citp.maudeSee the following PDF for the list of commands available in CITP, or read the Manual.
The followings are examples of specifications and proofs perfomed with CITP.
Simple proofs of two elementary inductive properties: the commutativity and associativity of the addition of natural numbers.
This example shows one possible way of dealing with generic lists (with potentially void elements) in CITP, including operations for appending lists, computing their lengths, or reversing lists. We prove that the append operation is associative and that, moreover, both the length and the reverse operations distribute over append.
Demonstrates the strength of the case analysis performed by CITP.
One agent puts repeatedly pairs < bit, d > of bits and encoded datas into a channel which automatically decodes the information.
When the agent reads < bit', d' > from the channel such that bit = bit', it is a confirmation that the data sent for decoding was received.
In thad case, the agent stores the data received into a list structure, alternates the bit, and selects the next encoded data for sending.
We assume that the channel is unreliable, meaning that the data in the channel may be lost or duplicated, but not exchanged or damaged.
Assume that many agents (or processes) are competting for a common resource, but that at any given moment of time only one agent can use the resource. That is, the agents exclude or prevent each other from accessing the resource. A protocol that can gurantee this kind of mutual-exclusion property is called a mutual exclusion protocol (slides).
As in the QLOCK example above, another protocol that can guarantee such a mutual-exclusion property is TAS, which makes use of shared lock and an atomic test & set operation. A diagrammatic representation of an execution of the protocol can be found here.
The protocol consists of two processes, Sender and Receiver, each having a data buffer and a one-bit state. Sender and Receiver use two channels to communicate with each other, as they do not share any common memory: (a) a data channel from Sender to Receiver for sending bit-packet pairs, and (b) an acknowledgement channel from Receiver to Sender for sending single bits for confirmation. The protocol works as follows:
< bit, pac > to the data channel, where bit is the Sender's bit and pac is the Sender's data to transmit.
If the Sender receives bit from Receiver over the acknowledgement channel, then that is a confirmation that the packet sent has been delivered.
In that case, Sender flips its bit and select the next packet to send.
< bit, pac > such that bit is different from its bit, then it stores pac and flips its bit.
Consider a scenario where arbitrarily many PCs are connected to a Cloud in order to exchange messages – for simplicity, we treat these messages as natural values. Each of the PCs can fetch the latest value from the cloud, compare it with their own value, and update the Cloud or their own value depending on which is larger; see the Cloud in images.
A proof of the fact that every connected graph has a spanning tree.