*g-program* as a multiplier.
Use it to verify the following M1 programs.
n down
to 0. You may assume n is a natural number. Prove
that the result is(/ (* n (+ n 1)) 2).
n down to 0. You may assume n is
a natural number. Prove that the result is (+ (/ (expt n 3) 3) (/ (expt n 2) 2) (/ n 6)).
n. (You will have to define factorial; it is not native
in ACL2.)
Fib(0) = 0 Fib(1) = 1 Fib(2) = Fib(1)+Fib(0) Fib(3) = Fib(2)+Fib(1) ...
Advice: M1 does not have recursion or method call, so you have to do
this iteratively. When you verify your helper function you will have to
think of the generalization that characterizes its output for all legal
inputs, not just the initial case. When you verify your loop code you'll
have to specify the final values of all of the locals you're using.
You could try to figure out the closed form expressions for the locals. But
a simpler approach is to define fib-locals to just return the
list of the final values of all the locals, computed exactly the way your
code does it.
n, is even
or odd. You may assume n is a natural number. To indicate
that n is even, leave 1 on the stack. Otherwise,
leave 0 on the stack.
Advice: A convenient expression of the idea ``n is even''
in ACL2 is the expression(equal (mod n 2) 0).
When n is a natural number, (equal (mod n 2) 0)
is t if n is even and is nil
if n is odd.
n. You
may assume that n is an integer. To indicate
that n is negative, leave -1 on the stack; to
indicate that n is zero, leave 0 on the stack; to
indicate that n is positive, leave +1 on the stack.
Prove that your program is correct.
n divided by d, where n
and d are natural numbers and d is not
0. Prove that your program is correct.
Advice: In ACL2, the floor of n divided by d
is (floor n d). For example, (floor 27 6)
is 4.
Warning: This program will require nested loops and hence is not strictly in the template you've been using. But perhaps you can figure it out.