[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

%%%%%%%%%%%%%%%%%%%%%%%%
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
```