How do I put proof obs onto operator args?

• To: larch-interest
• Subject: How do I put proof obs onto operator args?
• From: kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)
• Date: Tue, 08 Mar 94 11:55:50 -0800
• Cc: horning
• Delivery-Date: Tue, 08 Mar 94 11:57:18 -0800
• Sender: horning

[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?

Thanks to all who read this!

• How do I put proof obs onto operator args?
• From: leavens@bambam.cs.iastate.edu (Gary Leavens)

• Prev: Re: How do I put proof obs onto operator args?
• Next: LARCH THEOREM PROVER COURSE
• Index: Larch archive index