[Prev][Next][Index]
Re: Specifying the Reals in LSL?

Subject: Re: Specifying the Reals in LSL?

From: leavens@cs.iastate.edu (Gary Leavens)

Date: 29 Aug 95 17:35:00 GMT

Keywords: real numbers, LSL, computability, constraints

Newsgroups: comp.specification.larch

Organization: Iowa State University, Ames, Iowa

References: <leavens.809667621@bambam.cs.iastate.edu> <griffioe.809695828@news.cwi.nl>
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 500111040 USA / leavens@cs.iastate.edu
phone: (515)2941580 fax: (515)2940258 ftp site: ftp.cs.iastate.edu
URL: http://www.cs.iastate.edu/~leavens/homepage.html