CITP Manual

The Constructor-based Theorem Prover (CITP) is a tool for proving inductive properties of software systems specified with constructor-based logics. The present document describes the main commands supported by CITP.

Installing the CITP

The CITP uses Maude as rewriting engine. Hence, the first step is to download and install the Maude system following the instructions here. We present a basic introduction to Maude here.

Once Maude has been installed (we assume a maude command for executing it), we can download the CITP repository by using

git clone https://github.com/ittutu/CITP

This command creates a folder CITP in our computer. Among others, it contains the subfolder Tool, which contains the source code of the tool in the citp.maude file, and the subfolder Examples, with several examples that can be executed by users to test the tool. For example, to run the TAS example we should do as follows:

maude Tool/citp.maude

cd CITP/Examples/TAS
load tas.maude

select #CITP# .
loop init .

The first command starts Maude and loads the CITP. The second command sets the current folder as the one containing the tas example, while the third one loads the module into Maude. This module contains the simple mutual exclusion protocol test&set, which we will explain in detail later. Finally, the last two commands select the tool and initiate it, so we can start introducing commands.

Using the CITP

In the following we present how to introduce and prove goals in CITP. In Section Goals we present the syntax for goals. Then, in the next section we introduce the tactics that can be used to discharge these goals. Finally, we present some tips to take advantage of all the features implemented in CITP.

It is important to note that all the commands presented here must be introduced in the tool enclosed in parentheses, so they can be parsed by the CITP.

Goals

All proofs start by introducing a goal. In CITP, goals are sets of sentences related to a given module. The syntax for introducing goals is

goal MOD-NAME |-
SENT1 ;
...
SENTn ;

where MOD-NAME is the name of the module where the proof takes place and SENT1 ... SENTn are the sentences the goal is composed of. These sentences can be either equations, membership axioms, and rewrite rules.

Proof tactics

We present next the tactics available in CITP. In general, we will not apply single tactics but tactic lists of the form (tc1 ... tcn), where each tci is a single tactic.

Note that CITP handles a set of goals of the form (goal M |- SS), with M a module and SS a set of sentences. In contrast to other provers, CITP does not keep a tree structure and list of tactics will be applied to all goals.

If the user wants to apply the tactic list only to the current goal then the command (. tc1 ... tcn) can be used. Moreover, we can change the current goal with (select N), which selects the Nth goal as current one.

General proof tactics

The general proof tactics, described in the table below, are sound for all specifications. It is important to note that

Some details about these commands are:

• Simultaneous induction has syntax ind on V:Sort, for V:Sort a variable appearing in the goal. The cases are generated by using the operators marked with the ctor atribute in the specification.
• The theorem of constants replaces all variables by fresh constants and splits the sentences in the same goal in several goals.
• Case analysis splits the goals by using the conditions of conditional sentences. It assumes the conditions are disjointly true and the left-hand side of the sentences is equal.
• Implication adds the conditions in the sentences of the goal to the module.
• Reduction reduces by rewriting both sides of the current goal.
• Initialization has syntax init sen by sub, for a sentence sen and a substitution sub, gives concrete values to the variables in the sentence.
• Critical pairs left has syntax (cp-l sentence1 >< sentence2) tries to unify a subterm of sentence1 with the left-hand side of sentence2. cp-r works analogously for the right-hand side.

Tactic	Command
Simultaneous induction	ind on
Theorem of constants	tc
Case analysis	ca
Implication	imp
Reduction	red
Initialisation	init
Critical pairs left	cp-l
Critical pairs right	cp-r

Specific proof tactics

The specific proof tactics, listed in the table below, are sound for initial data types that are often used in applications such as sequences/lists, sets and pairs as long as they are protected.

It is important to note that these tactics are designed for goals consisting of a specification and a single formula: ca, tc, imp, red, cs, pair. However, if one of these tactics is applied to a goal of the form M |- {E1,...,En}, the goal is decomposed into a list of subgoals (M |- E1), ..., (M |- En) and then the tactic is applied to each goal M |- Ei.

Tactic	Command
Induction based on membership axioms	indx
Case analysis for sequences and sets	cs
Pair	pair

Interface commands

In addition to the commands for developing the proof, CITP provides commands for interacting with the interface, as shown by the table below.

Command	Description
rollback	Returns the proof process to the state before applying the last list of tactics.
show goals	Displays the goals to discharge.
show proof	Shows the sequence of lists of tactics applied
redTerm t	Reduces the term t to its normal form w.r.t. the current module.

Tips

In this section we present some syntax conventions useful for specifying and proving properties with CITP:

• CITP is well suited for finding inconsistencies in Booleans. For this reason, if we reach a module premises like ctor_i = ctor_j it might be useful to define conditional equations of the form ceq true = false if ctor_i = ctor_j.
• It might also worth defining goals as conditional equations, with the premises as conditions and the actual equation as conclusion.
• Although Maude provides a built-in predicate _==_, its semantics are not appropriate for theorem proving. If equalities are required, we recommend defining a new, commutative, predicate (CITP examples use _~_) with equations stating that X:Sort ~ X:Sort = true for all sorts and ctor_i ~ ctor_j = false for all constructors.
• In order to use the decision mechanisms for tuples they must be declared with syntax [_,...,_] or <_,...,_>.
• In order to use the decision mechanisms for multisets they must be defined with syntax __.
• If you try to prove the properties in the examples by yourself you may notice that some tactic lists are too long, in the sense that the property is proven before using all the tactics. We left these lists unmodified because we consider them standard strategies for proving goals and hence we decided to use them consistently for most examples; please feel free to modify them and find your own strategies.

Examples

We present some examples to illustrate the features implemented in CITP. We first present a simple example on natural numbers and then a more complex one on the specification of the TAS protocol.

PNat example

In this example we define natural numbers by using Peano axioms, which we use to define the addition and multiplication functions. Then, we prove that the addition is commutative and associative. The specification and the proofs are available here.

PNat specification

A Maude equational specification starts by fmod (standing for functional module), followed by the module name (PNAT in this case, from Peano Natural numbers), and is. Then, we can define the sorts, that in our case are PNat for natural numbers and PNzNat for non-zero natural numbers. Moreover, we can define a subsort relation between sorts; in our case we indicate that all the terms that have sort PNzNat have sort PNat as well:

fmod PNAT is
 sorts PNat PNzNat .
 subsorts PNzNat < PNat .

Next, we define constructors (ctor attribute) for our sorts, using operators that receive the arity and the co-arity. In our case 0 is the constructor for PNat and successor (s_, where the underscore is a placeholder) is the constructor for PNzNat.

 op 0 : -> PNat [ctor] .
 op s_ : PNat -> PNzNat [ctor].

If we do not use the ctor attribute then we are defining standard functions, like the addition and multiplication below. These functions have a prec attribute that indicate how high is their precedence: the lower the number the higher the precedence, so multiplication will be evaluated before addition:

 op _+_ : PNat PNat -> PNat [prec 33].
 op _*_ : PNat PNat -> PNat [prec 31].

Now, we define some variables of sort PNat to use in equations. The equations for addition are defined in the usual way; the first one indicates that adding a natural number to 0 returns the given natural number, while the second one applies addition recursively and then applies successor:

 vars M N P : PNat .

 eq 0 + N = N             [metadata "1"].
 eq s M + N = s(M + N)    [metadata "2"].

Note the use of the attribute metadata, that will allow CITP to identify equations. The equations for multiplication are defined in a similar way:

 eq M * 0 = 0           [metadata "3"].
 eq M * s N = M * N + M [metadata "4"].
endfm

PNat properties

In this section we show how to prove the associativity and commutativity of addition as defined above.

Previous lemmas

Before starting the main proof we state and prove two lemmas with particular cases for the commutativity:

(goal PNAT |-
eq M:PNat + 0 = M:PNat ;
eq M:PNat + s N:PNat = s(M:PNat + N:PNat);)

Note that the goal consists of two equations to be proved in the PNAT module. The natural way to proceed is to apply induction on M:

(ind on M:PNat)

This command creates two goals, one for each constructor of the sort. For example, the goal for the successor is:

--------------------- Goal: 1 ---------------------
< fmod PNAT is
sorts Bool PNat PNzNat .
subsort PNzNat < PNat .
op x#1 : -> PNat[metadata "induction-constant"].
eq M:PNat * 0 = 0[metadata "3"].
eq M:PNat * s N:PNat = M:PNat * N:PNat + M:PNat[metadata "4"].
eq 0 + N:PNat = N:PNat[metadata "1"].
eq x#1 + 0 = x#1[metadata "5" metadata "s_"].
eq x#1 + s N:PNat = s(x#1 + N:PNat)[metadata "6" metadata "s_"].
eq s M:PNat + N:PNat = s(M:PNat + N:PNat)[metadata "2"].
. . .
endfm,
eq s x#1 + 0 = s x#1 ;
eq s x#1 + s N:PNat = s(s x#1 + N:PNat); >
------------------- Current goal -------------------

It is interesting to see the new premises generated in the module by the induction command. For example, we have x#1 + 0 = x#1, which will be useful to discharge the first equation in the goal by combining it with the equation 2 for addition. We find similar premises to discharge the second equation. Hence, it is enough to apply the theorem of constants and reduction to prove both goals:

(tc red)

Commutativity

In order to use the lemmas above we need to create a new module importing PNAT in protecting mode (which indicates that no "junk" and no "confusion" is added to the module) and adding the lemmas as equations:

fmod PNAT-L is
 pr PNAT .
 vars M N : PNat .
 eq N + 0 = N          [metadata "lemma-1"].
 eq M + s N = s(M + N) [metadata "lemma-2"].
endfm

The goal is defined in this new module:

(goal PNAT-L |-
eq M:PNat + N:PNat = N:PNat + M:PNat ;)

It is enough to apply the same strategy we used above to prove this property:

(ind on M:PNat tc red)

Associativity

The associativity property does not require the lemmas. Hence, we just state the goal in the PNAT module:

(goal PNAT |- eq (X:PNat + Y:PNat)+ Z:PNat = X:PNat + (Y:PNat + Z:PNat);)

and use the tactics shown before to prove it:

(ind on X:PNat tc red)

TAS example

We present here a simple example to give users a flavor of how to specify systems in Maude and prove properties of them with the CITP. First, we describe how to specify the TAS protocol in Maude. Then, we prove properties on it with CITP. The specification of the protocol and the proofs are available here.

TAS specification

We first define the LABEL module to specify the possible states of processes: in remainder section (label cs) or in critical section (label cs). These operators are constructors (attribute ctor) of the sort Label. We also define a predicate _~_ for checking whether two labels are equal:

fmod LABEL is
 sort Label .

 ops rs cs : -> Label [ctor] .
 op _~_ : Label Label -> Bool [comm] .
 eq (L:Label ~ L:Label) = true .
 eq (rs ~ cs) = false .
endfm

The theory PID defines generic process identifiers (sort Pid) and the same equality predicate for them:

fth PID is inc BOOL .
 sort Pid .
 op _~_ : Pid Pid -> Bool [comm] .
 eq (P:Pid ~ P:Pid) = true .
endfth

The module STATUS specifies the states of the lock, which can be either open or close, constructors of the sort Status. We also define in this case the equality operator:

fmod STATUS is
 sort Status .
 ops open close : -> Status [ctor] .
 op _~_ : Status Status -> Bool [comm] .
 eq (L:Status ~ L:Status) = true .
 eq (open ~ close) = false .
endfm

The module TAS is in charge of defining the behavior of the system. It is parameterized by the theory PID above, imports the rest of modules, and defines a sort Sys for the system:

fmod TAS{X :: PID} is
 pr LABEL .
 pr STATUS .
 sort Sys .

We define next the constructors for the system. It can be in the initial state (init), a process identifier can be entering the critical section (enter) or leaving it (leave):

 --- any initial state
 op init : -> Sys [ctor] .
 --- transitions
 op enter : Sys X$Pid -> Sys [ctor] .
 op leave : Sys X$Pid -> Sys [ctor] .

We also define observations to observe the state of the system in a particular moment. The observation pc returns the label associated to the Pid given as argument, while lock returns the status of the lock:

 op pc   : Sys X$Pid -> Label .
 op lock : Sys -> Status .

We define some variables and start specifying the observations for the initial state. In this case all proceses are in the remainder section and the lock is open. Note that we use the attribute metadata to assign names to these equations. These names can be used later when proving properties with CITP:

 vars I J : X$Pid .
 var  S : Sys .

 eq pc(init,I) = rs   [metadata "CA-1"] .
 eq lock(init) = open [metadata "CA-A"] .

We define next observations for enter. We define pc first:

• The equation CA-PCE1 indicates that, if the lock is open and the process is in the remainder section, then it can go into the critical section.
• In any other case we need a recursive call:
  • Equation CA-PCE2 is applied when the processes are different.
  • Equation CA-PCE3 is applied when the process is not in the remainder section.
  • Equation CA-PCE4 is applied when the lock is closed.

Then, we define the equations for lock:

• The equation CA-LE1 indicates the lock changes to close when a process enters the critical section.
• Otherwise, we recursively traverse the system:
  • The equation CA-LE2 is applied when the process is not in the remainder section.
  • The equation CA-LE3 is applied when the lock was not open.

 ceq pc(enter(S,I),J) = cs      if J = I /\ pc(S,I) = rs /\ lock(S) = open [metadata "CA-PCE1"].
 ceq pc(enter(S,I),J) = pc(S,J) if (J ~ I) = false                         [metadata "CA-PCE2"].
 ceq pc(enter(S,I),J) = pc(S,J) if (pc(S,I) ~ rs) = false                  [metadata "CA-EPCE3"].
 ceq pc(enter(S,I),J) = pc(S,J) if (lock(S) ~ open) = false                [metadata "CA-PCE4"].

 ceq lock(enter(S,I)) = close   if pc(S,I) = rs /\ lock(S) = open [metadata "CA-LE1"].
 ceq lock(enter(S,I)) = lock(S) if (pc(S,I) ~ rs) = false         [metadata "CA-LE2"].
 ceq lock(enter(S,I)) = lock(S) if (lock(S) ~ open) = false       [metadata "CA-LE3"].

Finally, we define the behavior of the observations for leave. For pc we have:

• The equation CA-PCV1 indicates that the process goes to the remainder section when it was in the critical section.
• Otherwise, we recursively check the state:
  • The equation CA-PCV2 is applied when we are looking for a different process.
  • The equation CA-PCV3 is applied when it was not in the critical section.

Regarding lock, we have the following equations:

• The equation CA-LL1 indicates that the lock opens when the process goes out of the critical section.
• Otherwise, the equation CA-LL2 recursively checks the system:

 ceq pc(leave(S,I),J) = rs      if J = I /\ pc(S,I) = cs [metadata "CA-PCV1"].
 ceq pc(leave(S,I),J) = pc(S,J) if (J ~ I) = false       [metadata "CA-PCV2"].
 ceq pc(leave(S,I),J) = pc(S,J) if (pc(S,I) ~ cs) = false[metadata "CA-PCV3"].

 ceq lock(leave(S,I)) = open if pc(S,I) = cs              [metadata "CA-LL1"].
 ceq lock(leave(S,I)) = lock(S) if (pc(S,I) ~ cs) = false [metadata "CA-LL2"].
endfm

TAS properties

We show now how to prove some properties on this protocol. In particular, we prove that the lock is closed when there is a process in the critical section (first equation of the goal) and that, if two processes are in the critical section at the same time, it is because they are the same process (second equation):

(goal TAS |-
ceq lock(S:Sys)= close if pc(S:Sys,I:X$Pid)= cs[nonexec];
ceq I:X$Pid = J:X$Pid if pc(S:Sys,I:X$Pid)= cs /\ pc(S:Sys,J:X$Pid)= cs[nonexec];)

We start the proof by applying induction on S:Sys and reducing:

(ind on S:Sys red)

When this command is applied we obtain 3 new goals, one corresponding to each constructor for Sys. For example, CITP generates the following goal for leave:

====================================================
--------------------- Goal: 1 ---------------------
< fmod TAS is
sorts Bool Label Status Sys X$Pid .
op x#1 : -> Sys[metadata "induction-constant"].
op z#2 : -> X$Pid[metadata "induction-constant"].
ceq I:X$Pid = J:X$Pid if pc(x#1,I:X$Pid)= cs /\ pc(x#1,J:X$Pid)= cs[metadata "1" metadata "leave" nonexec].
ceq lock(x#1)= close if pc(x#1,I:X$Pid)= cs[metadata "2" metadata "leave" nonexec].
. . .
endfm,
ceq I:X$Pid = J:X$Pid if pc(leave(x#1,z#2),I:X$Pid)= cs /\ pc(leave(x#1,z#2),J:X$Pid)= cs[nonexec];
ceq lock(leave(x#1,z#2))= close if pc(leave(x#1,z#2),I:X$Pid)= cs[nonexec]; >
------------------- Current goal -------------------
====================================================

Note how the goals are listed after the current module, where only equations and operators generated by CITP are shown for the sake of readability.

We start proving the goal for init, so we select the appropriate goal:

(select 2)

which looks like follows:

< fmod TAS is
sorts Bool Label Status Sys X$Pid .
. . .
endfm,
ceq I:X$Pid = J:X$Pid if rs = cs /\ rs = cs[nonexec];
ceq open = close if rs = cs[nonexec]; >

This goal is proven by first applying the theorem of constants and implication:

(. tc red imp red)

once this tactic list is introduced, we obtain a couple of goals that looks like this:

< fmod TAS is
sorts Bool Label Status Sys X$Pid .
eq rs = cs [metadata "1"].
. . .
endfm,
eq open = close [nonexec]; >

We know that rs and cs are different and hence we have a contradiction. We use it to prove the property with the cp-l command:

(cp-l eq(rs ~ cs)= false ; >< eq rs = cs ;)

We continue the proof by applying the theorem of constants, case analysis, and implication:

(tc red ca-1 red ca red imp red)

This tactic list generates 20 goals, being the first one of them:

< fmod TAS is
sorts Bool Label Status Sys X$Pid .
op I#3 : -> X$Pid[metadata "new"].
op x#1 : -> Sys[metadata "induction-constant"].
op z#2 : -> X$Pid[metadata "induction-constant"].
eq I#3 ~ z#2 = false[metadata "3"].
eq cs ~ pc(x#1,z#2)= false[metadata "4"].
eq pc(x#1,I#3)= cs[metadata "5"].
ceq I:X$Pid = J:X$Pid if pc(x#1,I:X$Pid)= cs /\ pc(x#1,J:X$Pid)= cs[metadata "1" metadata "leave" nonexec].
ceq lock(x#1)= close if pc(x#1,I:X$Pid)= cs[metadata "2" metadata "leave" nonexec].
. . .
endfm,
eq lock(x#1)= close[nonexec]; >

We see that we have some free variables in the equations labeled as 1 and 2, so we can give them concrete values with the init command:

(init 2 by I:X$Pid <- I#3 red)

(init 1 by I:X$Pid <- I#3 ; J:X$Pid <- z#2 red)

These instantiations discharge 7 goals. The first goal that was not discharged is:

< fmod TAS is
sorts Bool Label Status Sys X$Pid .
op I#3 : -> X$Pid[metadata "new"].
op x#1 : -> Sys[metadata "induction-constant"].
op z#2 : -> X$Pid[metadata "induction-constant"].
eq I#3 = z#2[metadata "7"].
eq I#3 ~ z#2 = false[metadata "3"].
eq lock(x#1)= close[metadata "6"].
eq pc(x#1,I#3)= cs[metadata "5"].
eq pc(x#1,z#2)= cs[metadata "4"].
ceq I:X$Pid = J:X$Pid if pc(x#1,I:X$Pid)= cs /\ pc(x#1,J:X$Pid)= cs[metadata "1" metadata "leave" nonexec].
ceq lock(x#1)= close if pc(x#1,I:X$Pid)= cs[metadata "2" metadata "leave" nonexec].
. . .
endfm,
eq open = close[nonexec]; >

We notice that equations 3 and 7 are a contradiction, so we can join critical pairs again to discharge this goal:

(. cp-l 3 >< 7)

The rest of goals are easily discharged following the same ideas we have shown above:

(. cp-l eq(rs ~ cs)= false ; >< eq rs = cs ;)
(init 1 by I:X$Pid <- I#3 ; J:X$Pid <- J#4 red)
(. cp-l eq(open ~ close)= false ; >< eq open = close ;)
(. init 2 by I:X$Pid <- J#4)
(. cp-l eq(open ~ close)= false ; >< eq open = close ;)

References

• Michel Bidoit, Rolf Hennicker: Constructor-based observational logic. J. Log. Algebr. Program. 67(1-2): 3-51 (2006).
• Michel Bidoit, Rolf Hennicker, Alexander Kurz: Observational logic, constructor-based logic, and their duality00865-4). Theor. Comput. Sci. 3(298): 471-510 (2003).
• Kokichi Futatsugi, Daniel Gaina, Kazuhiro Ogata: Principles of proof scores in CafeOBJ. Theor. Comput. Sci. 464:90-112 (2012).
• Daniel Gaina, Kokichi Futatsugi, Kazuhiro Ogata: Constructor-based Logics. J. UCS 18(16): 2204-2233 (2012).
• Daniel Gaina: Interpolation in logics with constructors. Theor. Comput. Sci. 474: 46-59 (2013).
• Daniel Gaina, Kokichi Futatsugi: Initial semantics in logics with constructors. J. Log. Comput. 25(1): 95-116 (2015)
• Daniel Gaina, Zhang Min, Yuki Chiba, Yasuhito Arimoto: Constructor-based Inductive Theorem Prover. CALCO 2013, Warsaw, Poland, September 3-6 (2013).
• Daniel Gaina, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi: On Automation of OTS/CafeOBJ Method. Specification, Algebra, and Software: 578-602 (2014).