|
|
|
SearchNavigationUser login |
Alloy version of ACL2 binary adder example Date: Jan 10 2010 An Alloy description of a binary adder for numbers of arbitrary length, together with an assertion of its correctness. The model is based on an example given in Kaufmann, Manolios, and Moore's textbook 'Computer-Aided Reasoning: An Approach'; they give a definition of the adder and illustrate how to use ACL2 to prove it correct. The main interest of this model is the contrast between the ACL2 version's use of a recursive function on the one hand, and the Alloy model's use (in the absence of recursion) of purely declarative descriptions of sequences. (Note: both the definition of the serial adder and the predicate relating binary numbers to Alloy integers require more machinery than one might have expected; if readers see simpler and more direct ways to handle the problem, the author of the model would like to hear about them.)
|
The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.
Theme originally designed by Chris Herberte
An interesting exercise.
A potential solution to the definition of vc_sum as a function:
[Warning: I don't have immediate access to Alloy, so this is not machine tested.]
While Alloy won't allow a (singleton) set of sequences, it will allow a set of Int/VC pairs.
First version, which seems a bit of a cheat:
fun vc_sumf[a, b : Number]:seq VC{
{i : Int, b : Bit | some s : seq VC{i->b in s and vc_sum[a,b,s]}}
}
Now we produce a second version, by unfolding `vc_sum[a,b,s]' and eliminating s.
fun vc_sumg[a, b : Number]:seq VC{
{i : Int, v : VC {
0 <= i and i < max[#bits[a], #bits[b]]
v = (i = 0) implies half_adder[a.bits[0], b.bits[0]]
else (i > 0 and i < #a.bits and i < #b.bits ) implies full_adder[a.bits[i], b.bits[i], svc[i-1].carry]
else (i > 0 and i < #a.bits and i >= #b.bits) implies full_adder[a.bits[i], Zero, svc[i-1].carry]
else (i > 0 and i >= #a.bits and i < #b.bits ) implies full_adder[Zero, b.bits[i], svc[i-1].carry]
}
}
}
and, of course, we should:
check {all a, b : Number | vc_sumf[a, b] = vc_sumg[a, b]}
--
Jeremy L. Jacob Tel: +44-1904-43-2747 Fax: +44-1904-43-2767
Jeremy.Jacob@cs.york.ac.uk http://www-users.cs.york.ac.uk/~jeremy/
Dept. of Computer Science, The University of York, YORK, YO10 5DD, UK
Thank you for the comment. I'm glad you found the exercise interesting; I certainly enjoyed working it.
I've put your suggestions through Alloy, as well as I'm able, but have again run into difficulty.
In vc_sumf, I think
b : Bitappears to be a slip forv : VC; with that change, it seems to make perfect sense to me. The Analyzer, alas, highlights the first occurrence of 's' and issues the error message "A type error has occurred. Analysis cannot be performed since it requires higher-order quantification that could not be skolemized." I have not found a way to move the "some s : seq VC" out of the set comprehension for thei, vpairs.In vc_sumg, the problem is the residual references to
svc[n-1]. In the predicate formulation,svcis bound by the argument list, so the reference is legal. But I have not found a way to refer, in the body of a function expression, to (other parts of) the value of the expression being produced.I'm not sure whether we are bumping up against a crucial difference in the expressive power of Alloy functions and Alloy predicates here, or just failing to see a way to write the function we want. I confess that I'm glad I'm not the only one who ran into that higher-order quantification message, trying to write this function!
--C. M. Sperberg-McQueen
cmsmcq@blackmesatech.org
http://cmsmcq.com/mib