[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: indra@rug103.cs.rug.nl*Subject*: (Fwd) Strings*From*: "Dave Stringer-Calvert" <davesc@minster.cs.york.ac.uk>*Date*: Tue, 4 Nov 1997 12:23:41 +0000*Cc*: pvs-help@csl.sri.com

Here's Sam Owre's response to a similar question 2 years ago. Perhaps Sam or Shankar can comment further? Dave --- Forwarded mail from Sam Owre <owre@neon.csl.sri.com> To: davesc@minster.cs.york.ac.uk Dave, I was playing around with strings, trying to find a nice way to deal with them, and it looks like I have a reasonably nice solution. Here is the useful theory: string_lemmas: THEORY BEGIN l1, l2: VAR list[(char?)] f1, f2: VAR finseq[(char?)] c1, c2: VAR (char?) fseq_lem: LEMMA =[finseq[character]](list2finseq[(char?)](l1),list2finseq[(char?)](l2)) = (l1 = l2) cons_lem: LEMMA (cons(c1,l1) = cons(c2,l2)) = (c1 = c2 & l1 = l2) char_lem: LEMMA (c1 = c2) = (code(c1) = code(c2)) END string_lemmas Note that the actuals need to be carefully constructed. This will disappear in the future, but is needed for now. To use this theory, e.g., to prove rubbish in test : THEORY BEGIN IMPORTING string_lemmas C : string = "hello" D : string = "hellq" rubbish: THEOREM NOT C = D END test You simply issue (auto-rewrite-theory "string_lemmas") (auto-rewrite "C" "D") (assert) Note that you do *not* want to use grind (or auto-rewrite-defs), as this will expand list2finseq and make the rest of the proof difficult. Shankar and I have been talking about ways to make string handling nicer, so this will probably be obsolete before too long, but I thought you might be interested anyway. Cheers, Sam ---End of forwarded mail from Sam Owre <owre@neon.csl.sri.com> -- Dave Stringer-Calvert, MEng MACM, Department of Computer Science, University of York, Heslington, York, YO1 5DD. [+44|0] 1904 432764

- Prev by Date:
**equality on characters** - Next by Date:
**A question from Korea** - Prev by thread:
**Re: A question from Korea** - Next by thread:
**equality on characters** - Index(es):