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.
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.git
To use CITP, simply copy the file citp.maude to your current/working directory, open a terminal, and type:
If you are using the GitHub distribution, it suffices to open a terminal to the CITP directory and to type:
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.
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
bitis the Sender's bit and
pacis the Sender's data to transmit. If the Sender receives
bitfrom 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
bitis different from its bit, then it stores
pacand 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.