[Prev][Next][Index]

Re: Specifying the Reals in LSL?




W.O.D. Griffioen sends a trait, in which \A is used for universal
quantifiers, and \E for existential.
But I think the LSL checker is just interpreting \A and \E as
operators, since the variables n, n0, etc. still have to be declared
outside the equations.  It would seem that if the checker really understood
universal and existential quantification, then it should be able
to allow declarations of quantified variables just at the point
of use.  Perhaps it's just a bug in the LSL checker that
it doesn't insert quantified variables into its symbol table?

If you try using lsl (3.1beta3) on the following trait,
you'll get several errors of undeclared variables.
(This shows that just using \A and \E don't solve the syntax problem,
as far as I'm concerned.)

So I think either there is a bug in the LSL checker,
or in the syntax/semantics of LSL for using quantifiers in equations.
Or maybe it's not really supposed to work at all?
(If so, then we can't write this specification in LSL.)

Anyway, I've developed the example a bit more,
and thinks to Mark Vandevoorde for pointing out a typing
mistake I made earlier.

%%%%%%%%%%%%%%%%%%%%%%%%
MathSequence: trait

  includes Rational, Natural(Nat)

  introduces
    __[__]: MathSeq, Nat -> Q
    __+__, __*__: MathSeq, MathSeq -> MathSeq
    -__: MathSeq -> MathSeq
    __<=__: MathSeq, MathSeq -> Bool
    isCauchy, isZeroSequence: MathSeq -> Bool

  asserts
    \forall a,b: MathSeq, q: Q, i: Nat

       (a + b)[i] == a[i] + b[i];
       (a * b)[i] == a[i] * b[i];
       (-a)[i] == -(a[i]);

       a <= b
         == (\E n0: Nat                % error?
               (\A n: Nat               % error?
                  ((n >= n0) => a[n] <= b[n])));

       isCauchy(a)
         == (\A epsilon: Q               % error?
              (epsilon > 0 =>
                (\E n0: Nat               % error?
                   (\A n: Nat \A m: Nat    % error?
                     ((n >= n0 /\ m >= n0)
                       => abs(a[n] - a[m]) < epsilon)))));

       isZeroSequence(a)
         == (\A eqsilon: Q               % error?
              (epsilon > 0 =>
                 (\E n0: Nat               % error?
                   (\A n: Nat               % error?
                      ((n >= n0) => abs(c[n]) < epsilon)))));

   implies
      converts isCauchy, isZeroSequence,
                __<=__: MathSeq, MathSeq -> Bool
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%               

Of course, the syntactic problem is still unresolved in the above.

	Gary Leavens

--
	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/homepage.html