How do I put proof obs onto operator args?

• To: kirk@zipcode.Jpl.Nasa.Gov
• Subject: How do I put proof obs onto operator args?
• From: leavens@bambam.cs.iastate.edu (Gary Leavens)
• Date: Thu, 10 Mar 94 15:01:15 CST
• Cc: horning
• Delivery-Date: Thu, 10 Mar 94 13:09:45 -0800
• In-Reply-To: Kirk Reinholtz's message of Tue, 08 Mar 94 11:55:50 -0800 <9403081955.AA16941@roustabout.pa.dec.com>

   From: kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)
   Date: Tue, 08 Mar 94 11:55:50 -0800
   Sender: horning@src.dec.com
   X-Mts: smtp

   [Forwarded by horning@src.dec.com for kirk@zipcode.Jpl.Nasa.Gov]

   Say I have something like
   T tuple of a:A, b:B;
   op:T->T;
   ...
   op(t) == t_set(...);

   But I want all uses of op() to incur a proof obligation that
   some predicates on T hold (e.g. b has certain properties, or
   something)

   Am I going about this all wrong, or is there a way to state this,
   or is there a better paradigm, or what?

Kirk,
	I was hoping someone else would answer this, but I don't think
I understand the question.  This is at the LSL level (it looks like to me),
right?

Why doesn't it suffice to do something like...

Foo: trait
  T tuple of a:A, b:B
  assumes theProofObligationTrait
  introduces
    op: T -> T
	...
  asserts for all t:T
   op(t) == t_set(...)
	

... where the trait "theProofObligationTrait" would have to hold in each
case where this trait (Foo) is used?

Is there something more interesting going on?  (probably)

	Gary

• How do I put proof obs onto operator args?
• From: kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)

• Prev: FWD: call for papers on formal methods and standards
• Next: Re: How do I put proof obs onto operator args?
• Index: Larch archive index