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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Mon, 6 Jun 2016 20:56:47 +0200*References*: <82bc09bd-c5b9-4d2e-86d9-bfe4e86e4083@googlegroups.com> <cb211369-98e3-47a9-88e2-d99e63700f1b@googlegroups.com> <c93fcbd9-0b5a-4d2d-8594-d5f2be40d48d@googlegroups.com> <154DA5E2-B0B1-42FF-B9AC-249F0C53FFA3@gmail.com> <c782fde4-25bb-407f-8a26-34176a58f0ef@googlegroups.com> <4D492927-4F34-400C-9584-E1F36DFFEBC4@gmail.com> <afa3a800-5677-4b49-bca0-11e27eae1d96@googlegroups.com> <8C8A8418-DE56-4C0D-AA5C-0E2EA41C1484@gmail.com> <0848f9c1-7f68-4865-8ca0-3289110f8153@googlegroups.com>

THEOREM StackExistence == \A X : \E S,mt,ps,pp,tp : StackAxioms(X,S,mt,ps,pp,tp) You'll also want to prove StackAxioms(X, Stack(X), empty(X), ...) so that you can actually reason about the specification. In that sense, you need to prove well-definedness upfront – but of course, that doesn't mean that your specification is complete, since you can only rely on what the axioms assert. When you ASSUME the structure, you are not forced to justify the assumptions, although it would perhaps be good practice to make sure that you haven't introduced an inconsistency. Stephan |

**References**:**pvs, temporal logic and stacks***From:*fl

**Re: pvs, temporal logic and stacks***From:*Leslie Lamport

**Re: pvs, temporal logic and stacks***From:*Ron Pressler

**Re: [tlaplus] pvs, temporal logic and stacks***From:*Stephan Merz

**Re: [tlaplus] pvs, temporal logic and stacks***From:*Ron Pressler

**Re: [tlaplus] pvs, temporal logic and stacks***From:*Stephan Merz

**Re: [tlaplus] pvs, temporal logic and stacks***From:*Ron Pressler

**Re: [tlaplus] pvs, temporal logic and stacks***From:*Stephan Merz

**Re: [tlaplus] pvs, temporal logic and stacks***From:*Ron Pressler

- Prev by Date:
**specifying systems book, Figure 3.1 -- bug? -- seems impossible to receive in AsyncInterface** - Next by Date:
**Re: [tlaplus] specifying systems book, Figure 3.1 -- bug? -- seems impossible to receive in AsyncInterface** - Previous by thread:
**Re: [tlaplus] pvs, temporal logic and stacks** - Next by thread:
**Re: [tlaplus] pvs, temporal logic and stacks** - Index(es):