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

*To*: pvs-help@csl.sri.com*Subject*: problem with induction*From*: Christof Simons <simonsc@uni-muenster.de>*Date*: Sun, 13 Aug 2000 21:49:01 +0200*Delivery-Date*: Sun Aug 13 12:49:21 2000*Sender*: chris@uni-muenster.de

Hi! I have problems proving the theorem th. Thus I can't prove it, I think I did a mistake in my specificaton. Actually I wanted to build a finite array. The function t was intended to manipulate the array in the way, that every book which titel doesn't match the given string, is replaced by the constant none. Though the functions seem right to me, i can't prove the theorem by induction or measure-induct. Perhaps it's a totally wrong approach to the problem, but all I want is to change a finite array. Hopefully anyone can help me. greetings Chris

test: THEORY BEGIN max: posnat range: TYPE = {x: posnat | x <= max} book: TYPE = [# id: posnat, titel: string #] book_array: TYPE = [range -> book] none: book b: VAR book str: VAR string ba: VAR book_array i: VAR range low(str, ba, i): nat = i chg(str, ba, i): book_array = IF ba(i)`titel /= str THEN ba WITH [(i) := none] ELSE ba ENDIF rec(str, ba, i): RECURSIVE book_array = IF i = 1 THEN chg(str, ba, i) ELSE rec(str, chg(str, ba, i), i - 1) ENDIF MEASURE low t(str, ba): book_array = rec(str, ba, max) th: THEOREM ba(i) = b AND b`titel = str IMPLIES t(str, ba)(i) = b END test

- Prev by Date:
**No Subject** - Next by Date:
**problem with induction #2** - Prev by thread:
**problem with induction #2** - Next by thread:
**Need Help!** - Index(es):