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

*To*: hoffman@securecomputing.com (John Hoffman)*Subject*: Re: EXPAND and IF-THEN?*From*: John Hoffman <hoffman@securecomputing.com>*Date*: Thu, 29 Jan 1998 08:36:48 -0600 (CST)*Cc*: ddieckma@ececs.uc.edu, pvs-help@csl.sri.com*In-Reply-To*: <199801282336.RAA14393@mishra.sctc.com> from "John Hoffman" at Jan 28, 98 05:36:09 pm

> However, if you're bound and determined to proceed along this path of > proving everything at once, here's the proof file for the "first" > case, that avoids the evil pvs halting expansions. Note, however, > that in this case, the theorem isn't true, (you end up having to > show.... > > validCertificate = unknown > > which I'm assuming is false) The trick on proving complicated theorems > about record updates like you have here is to work "outside in." Then > when you get to a point where the field is updated, the rest of the > expansions can be ignored. > Bah, A good night's sleep caused me to see the light. The "first" case of your proof is valid, I'll append the proof. I didn't trying to prove the rest of your theorem. Primarily because I'm just blindly proving things, I've no idea how the proof is "supposed" to go. But the point is that if you don't expand everything at once, you can push the theorem through the theorem prover. Good luck, John ==============================++====================== John Hoffman, PhD || Secure Computing Corporation || Sushi is good? 2675 Long Lake Road || Life is good! Roseville, MN 55124 || hoffman@securecomputing.com || Fax :(612)628-2701 || - Origami Sushi Chef Phone:(612)628-2808 || ==============================++====================== -------------------- ("" (USE "initialAEGISServices") (FLATTEN) (SIMPLIFY) (SPLIT) (("1" (EXPAND "saneBoot") (EXPAND "getResource") (EXPAND "executeBootSequence") (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REPLACE -6) (HIDE -1 -2 -3 -4 -5 -6) (EXPAND "levelZeroBoot") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REVEAL -7) (REPLACE -1) (HIDE -1) (EXPAND "levelOneBoot") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REVEAL -8) (REPLACE -1) (HIDE -1) (EXPAND "levelTwoBoot") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REVEAL -9) (REPLACE -1) (HIDE -1) (EXPAND "levelThreeBoot") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REVEAL -10) (REPLACE -1) (HIDE -1) (EXPAND "levelFourBoot") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (EXPAND "executeService") (LIFT-IF) (SPLIT) (("1" (FLATTEN) (HIDE -1) (REVEAL -11) (REPLACE -1) (HIDE -1) (EXPAND "levelFiveBoot") (EXPAND "installAEGISResources") (EXPAND "installResource") (ASSERT) (REVEAL -1 -2 -3 -4 -5 -6 -7 -8 -9 -10) (SIMPLIFY) (EXPAND "integrityValid" -4) (EXPAND "getResource" -4) (EXPAND "getBootLevelResource" -4) (EXPAND "installAEGISResources" -4) (EXPAND "installResource" -4) (PROPAX)) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)))) ("2" (POSTPONE)) ("3" (POSTPONE)) ("4" (POSTPONE)) ("5" (POSTPONE))))

**References**:**Re: EXPAND and IF-THEN?***From:*John Hoffman <hoffman@securecomputing.com>

- Prev by Date:
**Re: EXPAND and IF-THEN?** - Next by Date:
**PROGRAM-ERROR using inst?** - Prev by thread:
**Re: EXPAND and IF-THEN?** - Next by thread:
**Recursive declarations** - Index(es):