**Time:** Tuesday and Thursday, 9:30-10:45

**Place:** Siebel Center 1131

**Professor:** José Meseguer

**Office Hours:** Immediately following class in Dr. Meseguer's office.

**TA:** Everett Hildenbrandt (hildenb2@illinois.edu)

- (STACS) Set Theory and Algebra in Computer Science.
- Peter Ölveczky's book Formal Modeling and Analysis of Distributed Systems (contact course TA for copy of pre-print).
- Algebraic Semantics of Imperative Programs, by Goguen, Malcolm.
- Maude 2.7 Manual.
- Constructor-Based Reachability Logic for Rewrite Theories.

The course will consist of weekly homework assignments and one long homework assignment towards the end covering a wide range of the course material. Each problem on each homework will be worth 10 points, and the homeworks all together will be worth 70% of the grade. The final comprehensive homework assignment will be worth 30% of the grade.

If you are taking the class for 4 credits, then there will also be a final project for the course. The final project must be turned in by the assigned final date before a grade for the class will be issued.

Instructions for the Maude ITP are provided below.

- What is program verification?
- How can we do program verification?
- What types of programming languages will we be able to perform verification over?
- How will we represent programming languages and programs mathematically?

- Introduction to equational theories.
- Unsorted/many sorted/order sorted theories.
- Maude functional modules as many-/order-sorted equational theories.

Pictures:

- Many-sorted signature as a labelled multi-graph
- Unary many-sorted signatures are labelled graphs
- Order-sorted signature for lists of naturals

- Introduction to algebras (as interpretations of equational theories).
- Order sorted signatures, sensibility/preregularity of order-sorted signatures.
- The term algebras
*T*_{Σ}and*T*_{Σ(X)}(extension with variables). - Variable substitutions and equations.

Pictures:

- Many-sorted signature of a vector space
- Set membership vs normalized-distribution interpretation of boolean algebra

- Subterms, term contexts, and term decompositions.
- Equational theories as sets of universally quantified equations.
- Equational deduction as replacing equals by equals using matching and substitution.
- Term rewrite relations as a deduction calculus for equations.
- Rewriting modulo built-in structural theories.

- Executability conditions of a rewriting definition:
- No extra variables in RHS of rule
*Sort decreasing*: Rewriting decreases the sorts of things in general.*Confluence*(determinism): Rewriting with any rules in any order works. This is also said as: satisfies the Church-Rosser joinability property.*Terminating*: Rewriting eventually stops.

- Add axioms
*B*, get quotient system*E*/*B*; extend all above ideas to the modulo*B*case. - Given that the above are satisfied, you get the
*Canonical Term Algebra*. This is the algebra that you compute using rewriting (eg. what Maude does). - If the canonical term algebra does not contain some symbol
*f*, than that symbol is not in the*constructor subsignature*. *Free*constructors have no equations or axioms with them as the top-level symbol;*non-free*ones do.

- Local confluence
- Church-Rosser Checker

Lecture Slides A Lecture Slides B

If you are having trouble with the tools on your machine, try using the EWS Linux machines as well. To access the EWS servers, simply (replace NETID with your net-id):

```
$ ssh NETID@linux.ews.illinois.edu
NETID@ssh.courses.engr.illinois.edu's password:
Last login: Mon Oct 2 17:48:55 2017 from linux-a2.ews.illinois.edu
[NETID@engr-courses-li ~]$
```

Maude will be the primary tool used in this course, but several tools/libraries written in Maude will also be used. Some of these libraries require extra functionality to be added directly to Maude (at the C++ level). You can choose to build from the Maude sources or directly from binary releases of Maude 2.7.1.

```
# Download and unzip Maude 2.7.1 binary release for Linux
$ wget 'https://github.com/maude-team/maude/releases/download/v2.7.1-ext-hooks/maude-2.7.1-linux.tar.gz'
$ tar -xvf maude-2.7.1-linux.tar.gz
# Download Maude 2.7.1 binary release for MacOS
$ wget 'http://maude.cs.illinois.edu/w/images/2/25/Maude-2.7.1-osx.zip'
$ unzip Maude-2.7.1-osx.zip
# Run Maude
$ ./maude
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.7.1 built: Aug 31 2016 18:22:38
Copyright 1997-2016 SRI International
Sun Oct 1 11:59:31 2017
Maude>
```

The MFE packages together several tools which will be used in the course. It's recommended that you use the binary releases for anything needing the MFE. To get setup using MFE, you might do:

```
# Clone MFE
$ git clone 'https://github.com/maude-team/mfe'
# Launch Maude with MFE
$ ./maude mfe/src/mfe.maude
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.7.1 built: Aug 31 2016 18:22:38
Copyright 1997-2016 SRI International
Sun Oct 1 11:51:55 2017
Full Maude 2.7e September 22th 2016
The Maude Formal Environment 1.0b
Inductive Theorem Prover - July 20th 2010
Sufficient Completeness Checker 2a - August 2010
Church-Rosser Checker 3p - August 30th 2016
Coherence Checker 3p - August 30th 2016
Maude Termination Tool 1.5j - August 11th 2014
Maude>
```

Note that many of the tools in the MFE *cannot* reason with built-in modules (many of the modules which come in `prelude.maude`

). By default though, Maude includes the built-in module `BOOL`

with any user-defined module. If you get the following error:

`Error The use of built-ins is not supported by the checker.`

be sure to disable including `BOOL`

into your module by default:

```
set include BOOL off .
fmod MYMODULE is
...
endfm
```

If you are in loop mode (eg. if you have already loaded the MFE), then you must do this in parentheses:

```
(set include BOOL off .)
(fmod MYMODULE is
...
endfm)
```

The AvCRPO tool can be used to prove a set of equations *E* over some signature *Σ* terminating modulo associative/commutative axioms. It does this by building an axiom-aware recursive-path-ordering on terms (using hints provided by the user) and showing that each equation is well-founded given this ordering. An example setup/running of the tool might look like:

```
# Download and unzip AvCRPO Maude files
$ wget 'https://courses.engr.illinois.edu/cs476/fa2017/tools/acrpo-tool-distribution.zip'
$ unzip acrpo-tool-distribution.zip
# Run AvCRPO tool on provided example
$ ./maude
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.7.1 built: Aug 31 2016 18:22:38
Copyright 1997-2016 SRI International
Sun Oct 1 12:18:30 2017
# Load `NATU` signature file (where the signature module is named `TEST`)
Maude> load acrpo-tool-distribution/sig-natu.maude
# Load file with AvCRPO tool in it
Maude> load acrpo-tool-distribution/acrpo.maude
# Load file which checks that each equation in module `NATU` is well-founded
# using the ordering supplied in `TEST` module
Maude> load acrpo-tool-distribution/check-natu.maude
==========================================
reduce in ACRPO-EXT : (0 + X:Natu) >AC X:Natu .
rewrites: 3123 in 3ms cpu (3ms real) (1041000 rewrites/second)
result @#Bool#@: @#true#@
==========================================
reduce in ACRPO-EXT : (X:Natu + s(Y:Natu)) >AC s(X:Natu + Y:Natu) .
rewrites: 332 in 1ms cpu (0ms real) (332000 rewrites/second)
result @#Bool#@: @#true#@
==========================================
reduce in ACRPO-EXT : (X:Natu * 0) >AC 0 .
rewrites: 54 in 0ms cpu (0ms real) (~ rewrites/second)
result @#Bool#@: @#true#@
==========================================
reduce in ACRPO-EXT : (X:Natu * s(Y:Natu)) >AC (X:Natu + (X:Natu * Y:Natu)) .
rewrites: 284 in 0ms cpu (0ms real) (~ rewrites/second)
result @#Bool#@: @#true#@
==========================================
reduce in ACRPO-EXT : (X:Natu ^ 0) >AC s(0) .
rewrites: 91 in 0ms cpu (0ms real) (~ rewrites/second)
result @#Bool#@: @#true#@
==========================================
reduce in ACRPO-EXT : (X:Natu ^ s(Y:Natu)) >AC (X:Natu * (X:Natu ^ Y:Natu)) .
rewrites: 281 in 0ms cpu (0ms real) (~ rewrites/second)
result @#Bool#@: @#true#@
Maude>
```

`acrpo-tool-distribution/natu.maude`

contains the original module`NATU`

which we wish to prove terminating.`acrpo-tool-distribution/sig-natu.maude`

contains the hints about how to build the recursive-path-ordering for the signature of`NATU`

(in a module called`TEST`

).`acrpo-tool-distribution/check-natu.maude`

contains the queries which check that each equation is well-founded given the ordering generated by the tool.

The SCC tool works on an older version of Maude, and I only know of Linux binaries for it. Login to EWS or use a virtual machine if you are not on a Linux machine.

```
$ wget 'http://maude.cs.uiuc.edu/tools/scc/releases/Maude-ceta-2.3-linux.tgz'
$ tar -xvf Maude-ceta-2.3-linux.tgz
$ cd Maude-ceta-2.3-linux
$ ./maude-ceta
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude-ceta 2.3 built: Feb 18 2007 09:49:47
Copyright 1997-2007 SRI International
With CETA extensions Copyright 2006-2007
University of Illinois at Urbana-Champaign
Mon Oct 2 19:17:22 2017
# Load SCC
Maude> load scc.maude
# Start the SCC
Maude> loop init-cc .
Starting the Maude Sufficient and Canonical Completeness Checker.
# Load the file with module of interest (note that it should NOT be in parens)
Maude> load ../../../PATH/TO/FILE/WITH/MODULE/NOT/IN/PARENTHESES
# Select the CC-LOOP module.
Maude> select CC-LOOP .
# Check Sufficient Completeness (modulo other proof goals)
Maude> (scc MODULE-OF-INTEREST .)
Warning: no loop state.
Advisory: attempting to reinitialize loop.
Starting the Maude Sufficient and Canonical Completeness Checker.
Checking sufficient completeness of MODULE-OF-INTEREST ...
Success: MODULE-OF-INTEREST is sufficiently complete under the assumption that it is ground weakly-normalizing, confluent, and ground sort-decreasing.
```

Go to the Maude ITP Webpage to download the sources for the Maude ITP. The Maude ITP runs on Maude 2.7.

Commands that you may find useful (see the tutorial on the Maude ITP website):

`ind`

for doing structural induction on a variable.`auto`

for discharging goals with rewriting.`cns`

for using the lemma of constants.`imp`

for handling implications.`enable`

and`disable`

for enabling/disabling rewriting with given rules. Note that some of the other commands may add equations to the module in question. For example, when using the`(imp .)`

command on goal`u = v ==> phi`

, the equation`u = v`

will be added to the module (assumed as true) and`phi`

will be the new proof goal. No check is made that these added equations don't loop forever, so it may be necessary to`disable`

those equations from consideration.

Using the example module from lecture 13 (say file `nat-ord.maude`

):

```
fmod NATURAL-ORD is
sort Natural .
op 0 : -> Natural [ctor] .
op s : Natural -> Natural [ctor] .
op _<_ : Natural Natural -> Bool .
op _=<_ : Natural Natural -> Bool .
vars N M : Natural .
eq N < 0 = false .
eq 0 < s(N) = true .
eq s(N) < s(M) = N < M .
ceq N =< M = true if N < M .
ceq N =< M = true if not(M < N) .
ceq N =< M = false if M < N .
endfm
```

And an example interaction:

```
# Download and unpack the Maude itp
$ wget 'http://maude.cs.uiuc.edu/tools/itp/maude_itp.tar.gz'
$ tar -xvf maude_itp.tar.gz
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.7 built: Oct 17 2017 22:51:54
Copyright 1997-2014 SRI International
Tue Oct 17 23:40:31 2017
Maude> load maude_itp/itp-tool.maude
Maude> load nat-ord.maude
Maude> select ITP-TOOL .
Maude> loop init-itp .
ITP tool (May 25th, 2006)
--- Introduce linearity goal
--- ------------------------
Maude> (goal linear : NATURAL-ORD |- A{N:Natural ; M:Natural} (((N =< M) or (M =< N)) = (true)) .)
rewrites: 1200 in 18ms cpu (18ms real) (66666 rewrites/second)
=================================
label-sel: linear@0
=================================
A{M:Natural ; N:Natural}
N:Natural =< M:Natural or M:Natural =< N:Natural = true
+++++++++++++++++++++++++++++++++
--- Use lemma of constants
--- ----------------------
Maude> (cns .)
rewrites: 223 in 3ms cpu (2ms real) (74333 rewrites/second)
New goals:
=================================
label-sel: linear@0
=================================
N*Natural =< M*Natural or M*Natural =< N*Natural = true
+++++++++++++++++++++++++++++++++
--- Split on N < M
--- --------------
Maude> (split on (N*Natural < M*Natural) .)
rewrites: 222 in 5ms cpu (5ms real) (44400 rewrites/second)
New goals:
=================================
label-sel: linear@1.0
=================================
N*Natural =< M*Natural or M*Natural =< N*Natural = true
=================================
label: linear@2.0
=================================
N*Natural =< M*Natural or M*Natural =< N*Natural = true
+++++++++++++++++++++++++++++++++
--- Discharge goal 1 with assumptions
--- ---------------------------------
Maude> (auto .)
rewrites: 112 in 0ms cpu (0ms real) (~ rewrites/second)
Eliminated current goal.
New current goal:
=================================
label-sel: linear@2.0
=================================
N*Natural =< M*Natural or M*Natural =< N*Natural = true
+++++++++++++++++++++++++++++++++
--- Discharge goal 2 with assumptions
--- ---------------------------------
Maude> (auto .)
rewrites: 54 in 0ms cpu (0ms real) (~ rewrites/second)
Eliminated current goal.
q.e.d
+++++++++++++++++++++++++++++++++
```