Formally Speaking

Formal methods in software engineering and teaching computer science

New Role Model

Tea Leoni as Dr. Elizabeth Adams McCord in the TV show Madam Secretary. At this point she is a professor of history at the University of Virginia…


Alloy to the rescue

In my course Formal Methods in Software Engineering, I spend a few weeks reviewing formal logic. I like to give an assignment where I make the students play the role of human validity-checker/model-finder. In these questions I specify a first order vocabulary; a context, i.e., a set of formulas assumed to hold; and a query, which is another formula. The goal is to determine whether the query is valid, i.e., will it evaluate to true under all models in which all of the context formulas evaluate to true. In case it is not valid, an explicit counter-model must be provided, i.e., a model in which the context holds but the query doesn’t.

Here is one of the problems: the vocabulary consists of a single constant c, and a predicate P and function f, both of arity 2.

  • Context:
    1. \forall x,y. P(f(x,y), f(y,x))
    2. \forall x.\exists y. P(f(x,y), c)
  • Query: \exists x.P(f(x,c),c).

I’m not sure what I was thinking when I made up that problem, but I probably thought I had a proof that it was valid — perhaps I meant to add another formula to the context. In any case, when I looked at it again the day the assignment was due, I couldn’t figure it out. On the one hand, I didn’t think it was valid, on the other, all my attempts to come up with a model failed. (You might try to answer this question yourself before reading further.)

So I tried asking CVC4, an automated theorem prover which we had covered in class. Here is the input file:

p : (T,T) -> BOOLEAN;
f : (T,T) -> T;
c : T;

ASSERT FORALL (x,y:T): p(f(x,y),f(y,x));
ASSERT FORALL (x:T): EXISTS (y:T): p(f(x,y),c);
QUERY EXISTS (x:T): p(f(x,c),c);

And CVC4’s terse response:

unknown (INCOMPLETE)

This really isn’t that surprising: the validity question for FOL is undecidable in general, and in my experience CVC4 (and most SMT-style theorem provers) usually have trouble with all but the simplest queries involving quantifiers.

In class, the students were in an uproar—apparently they all spent hours trying to solve this problem, had tried CVC4 unsuccessfully, just as I had — and none of them could come up with a proof or counter-model. They were really curious about the answer. I had to admit I didn’t know! — and went on with the lecture — about Alloy.

Somewhere near the end of the lecture it struck me we might use Alloy to answer that question. With 5 minutes to go, I whipped up the following Alloy model:

abstract sig Bool {}
one sig T, F extends Bool {}

sig U {
  f : U -> U,      -- function from UxU to U
  P : U -> Bool    -- function from UxU to Bool ("predicate")

one sig c in U {}

fact {
  all x,y : U | one f[x,y]
  all x,y : U | one P[x,y]
  all x,y : U | P[f[x,y],f[y,x]]=T
  all x : U | some y : U | P[f[x,y],c]=T

assert query {
  some x : U | P[f[x,c],c]=T

check query for 3

I’m constantly surprised by the flexibility of the Alloy language. It has been used to represent such a wide variety of domains. Once you get the hang of it, it is quite easy to use. Like CVC4, the checking/solving part is fully automatic. Unlike CVC4, Alloy can’t really prove things — for example, it cannot prove that the query above is valid. Instead, the user specifies a bounded scope, which in this case means placing an upper bound on the size of the domain U. With bounded scope, the validity problem becomes decidable: assuming you don’t run out of memory (or patience), Alloy can tell whether or not there exists a model within the scope satisfying the specified properties, and in the case where such a model does exist, it will show you one (or all) of them. The magic works by converting the problem to a boolean satisfiability (SAT) problem, which is passed off to a standard SAT solver; if the SAT solver reports the formula is satisfiable, Alloy translates the solution back to an instance of your Alloy model.

Here is a really interesting recent application of Alloy: Pamela Zave of AT&T Labs used Alloy to investigate the Chord protocol, a widely-used distributed hash-table algorithm. Published papers about chord specify the algorithm carefully and “prove” (in the traditional informal sense) it satisfies several properties. Using Alloy, Dr. Zave discovered that none of those properties actually holds. She also showed how to fix Chord to make it correct. If you happen to be in Delaware on Friday, Nov. 6, 2015 come to the SIG-SYS seminar (12:15 PM, Smith Hall, Room 101), where Dr. Zave will be talking about this work.

Back to the FOL assignment: Alloy found a counter-model with U of size 3 (but not less than 3). It took less then two tenths of a second. Here it is: U=\{0,1,2\}, c=2, and

\begin{array}{cccc}      x & y & f(x,y) & P(x,y) \\ \hline      0 & 0 & 1 & \textbf{T} \\      0 & 1 & 0 & \textbf{T} \\      0 & 2 & 1 & \textbf{T} \\      1 & 0 & 1 & \textbf{T} \\      1 & 1 & 2 & \textbf{T} \\      1 & 2 & 1 & \textbf{F} \\      2 & 0 & 0 & \textbf{T} \\      2 & 1 & 1 & \textbf{T} \\      2 & 2 & 1 & \textbf{T}    \end{array}

We checked by hand that the context holds and the query doesn’t in this model.

The students now have an admiration for Alloy bordering on awe….I wish I could say I planned it that wayūüėČ

A question about Abstract Interpretation

This note deals with Section 7 of Cousot and Cousot, Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL, 1977.

First, the context: at this point in the paper, the notion of refinement of abstract interpretations has already been defined: suppose I=\langle\textsf{Cont},\ldots\rangle and \overline{I}=\langle\overline{\textsf{Cont}},\ldots\rangle are two abstract interpretations.   Suppose \alpha\colon \textsf{Cont}\rightarrow\overline{\textsf{Cont}}, and \gamma\colon\overline{\textsf{Cont}}\rightarrow \textsf{Cont} satisfy (6.2) \alpha and \gamma are order-preserving, (6.3) \overline{x}=\alpha(\gamma(\overline{x})) for all \overline{x}\in\overline{\textsf{Cont}}, and (6.4) x\leq\gamma(\alpha(x)) for all x\in\textsf{Cont}.  We then write I\leq(\alpha,\gamma)\overline{I}.  We write I\leq\overline{I}, and say I is a refinement of \overline{I}, if there exist maps \alpha and \gamma such that I\leq(\alpha,\gamma)\overline{I}.

Section 7 begins by pointing out that \leq is reflexive and transitive and then defines I\equiv I' to mean I\leq I' \wedge I'\leq I. The authors point out that \equiv is an equivalence relation, which is not hard to see. (One quibble: I thought an equivalence relation required a set, and I don’t see why the class of all abstract interpretations of a program is a set. But ignore this for now.)

So far, so good.  But then comes the statement

We have:
\{I\equiv(\beta) I'\} \Leftrightarrow \{\beta\ \text{is an isomorphism between the algebras}\ I\ \text{and}\ I'\}
The proof gives some insight in the abstraction process :

I assume the word “algebra” in this context means “boolean algebra”, so that \beta\colon\textsf{Cont}\rightarrow\textsf{Cont}' is an invertible map preserving order, etc. ¬†¬†But what is the meaning of “I\equiv(\beta) I'“? I don’t believe this notation has been defined. At first, I thought the excerpt above was the definition, but that can’t be right because then there would be no need for a proof! ¬†Now, even though I am not sure what this notation means, and therefore I don’t know what the authors are trying to prove, it seems that the bulk of the proof (the part beginning “2 – reciprocally”) is an attempt to show the following: if I\equiv I' then I and I' are isomorphic algebras.

The argument can be summarized as follows: suppose I\leq (\alpha_1,\gamma_1)I'. To simplify the notation, I is identified with the set \textsf{Cont} (and ditto for I'). It can be shown that \alpha_1|_{\gamma_1(I')} (the restriction of \alpha_1 to the set \gamma_1(I')) is a bijection from \gamma_1(I') to I'.   Supposing also that I'\leq(\alpha_2,\gamma_2)I, we have \alpha_2|_{\gamma_2(I)} is a bijection from \gamma_2(I) to I.  From this, the authors conclude

\alpha_1|_{\gamma_1(I')} \circ \alpha_2|_{\gamma_2(I)} is a bijection between \gamma_2(I) and I'.

The problem with this is that the composition \alpha_1|_{\gamma_1(I')} \circ \alpha_2|_{\gamma_2(I)}
is not defined, since the image of \alpha_2|_{\gamma_2(I)} is I, which is not necessarily contained in \gamma_1(I'), the domain of \alpha_1|_{\gamma_1(I')}. There are other points in the proof that do not make sense to me, but this is enough to ruin the show.  (The proof then uses this claim to argue \alpha_1 is a bijection from I to I', yielding the desired algebra isomorphism.)

To make this concrete, let S=\gamma_1(I') and S'=\gamma_2(I). The authors have shown that \alpha_1|_{S} is a bijection from S to I' and that \alpha_2|_{S'} is a bijection from S' to I. From this, they try to conclude that \alpha_1 is a bijection from I to I'. A counterexample to this claim is obtained by letting I=I'=\mathbb{Z} and S=S'=2\mathbb{Z}. Define \alpha_i(n)=\lfloor n/2\rfloor (i=1,2). Then \alpha_i|_{2\mathbb{Z}} is a bijection from 2\mathbb{Z} to \mathbb{Z}, but \alpha_i is not a bijection from \mathbb{Z} to \mathbb{Z}.

Now, it could be that I am just missing something, and if so, I would appreciate any clarification. And I would still like to know whether the statement “if I\equiv I' then I and I' are isomorphic algebras” is a theorem.