Sandro: We need to be doing these discussions on the list, and I am replying accordingly. The reason I replied only to you before is that you failed to send your note to the list!
All: The partial context here is quoted by Sandro at bottom. It was a note in which I was talking about the difference between the expressiveness of pre/post conditions and verification. Basically, pre/post can only speak about things that are reachable from "inside" the program, and only those that can be articulated within the current lexical contour. Verification can potentially explore properties about the overall state of the program. On Mon, Mar 22, 2010 at 10:57 AM, Sandro Magi <[email protected]> wrote: > 1. no-gc looks like a global property that you currently verify > piecewise by effect analysis, then check the inferred effect at > top-level: if an effect was incurred and no effect was required, fail, > otherwise no GC was used. Parametric effect analysis would just > propagate the required effect constraints globally (or perhaps effects > are insufficiently fine-grained or unusable?). Yes. No-GC, and effect-like properties in general, have a natural modular expression. The only real problem I see with effect-like properties is a usability issue: effect systems seem to work mainly because the compiler knows what effects are under discussion and is able to locally discharge most of them down to concrete resolutions. If we wanted to add user-defined effects, it becomes necessary to preserve all of the effect dependency equations visibly within the type of each procedure/function. > 2. For global data type invariants, how are abstract data types > insufficient? You encapsulate the desired properties in an abstract > type, or refine an existing abstract type with additional constraints > ala refinement types, and enforce the invariants via the constructors. > This was the thrust behind lightweight static capabilities [1], and > refinement types make this even more powerful. > > Or perhaps the properties you're considering don't have a meaningful > expression as a value? Would this preclude trying to express this > property as a phantom type of some abstract "program" type? You're asking the right question, but you're into a domain where I don't know enough to answer. Let me give two examples of properties I would like to encode: 1. If I am reading/writing some field of this struct, then that lock over there must be held. Problem: the lock in question may not be lexically nameable in the current context. I suspect that this one can be done with phantom types or phantom values of some sort, but I don't know. 2. I hold a pointer to an object of type Mumble. At some previous time in the execution, I have run some sanity check on that object to ensure that it is in some desired state. I need to show that at no point in the current execution between the establishment of the desired state and the current sequence point did I run some deconditioning operation that might "break" that state. It's okay to have done so if I abandoned the computation in an orderly way; just not if I get to the place where I rely on the condition I previously checked. > On 22/03/2010 1:26 PM, Jonathan S. Shapiro wrote: >> Jonathan doesn't quite /know/ what he wants at this point. Not clear if >> this is a case of simple exhaustion or the result of improving >> understanding. :-) >> >> One thing I looked at while at Microsoft was the Contracts extension in >> .Net. This provides the traditional preconditions, postconditions, and >> assertions for .Net programs. There is much talk about discharging these >> statically, and little demonstration as yet. It seems very hard to do >> that discharge given that (a) these things aren't part of type, and (b) >> dynamic class loading can violate just about any assumption. >> >> But there is a bigger issue with pre/post-conditions. A pre/post is an >> expression. Ignoring some syntactic hackery in the postcondition >> identifier syntax, the conditions can only refer to identifiers and data >> structures that are in scope at the point where the condition appears. >> In particular, you can't do any sort of quantification over the program >> state. >> >> Conditions in this form are good to have, and they can /always/ be >> discharged by checking them at runtime, but they can only speak in terms >> of information that is "in band" w.r.t. the current execution. So they >> only let you express verification conditions that can be stated within a >> given lexical scope. >> >> Which leaves the question: how do we express over-arching /global/ >> properties. For example: a property that is supposed to hold at all >> sequence points in a program, except where suspended? Alternatively put: >> how do we confirm that our desired global properties are enforced by the >> local properties that we have chosen to express? This is the point >> where classical pre/post conditions fall over, and you more or less >> /have/ to resort to whole-program proof. >> >> So I am coming to think that there is a line here, and that certain >> properties /shouldn't/ be discharged by the compiler. The question then >> becomes: should the source language provide sufficient means to document >> those properties via some appropriate meta-language? I don't yet feel >> that I have an answer to that. >> >> Perhaps there is a way to look at pre/post that I don't yet understand. >> In a perfect world, I'ld love to go spend a year visiting the types and >> programming languages group at Penn while I straighten my head out. :-) >> >> >> shap > > > _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
