From: xorque <xorquewasp@googlemail.com>
Subject: SPARK left/right shift.
Date: Tue, 21 Jul 2009 02:07:40 -0700 (PDT)
Date: 2009-07-21T02:07:40-07:00 [thread overview]
Message-ID: <9d0eb92b-bb21-40eb-ac6d-2e1e829b95cc@s15g2000yqs.googlegroups.com> (raw)
Hi.
What's the "correct" way to get access to left/right shift operations
for modular types in SPARK? I see from the Checker manual that
the proof language is capable of modelling them but then I also see
that the Interfaces package isn't predefined.
next reply other threads:[~2009-07-21 9:07 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-07-21 9:07 xorque [this message]
2009-07-21 9:21 ` SPARK left/right shift Rod Chapman
2009-07-21 9:31 ` Rod Chapman
2009-07-21 9:38 ` xorque
2009-07-21 9:54 ` Rod Chapman
2009-07-21 10:00 ` xorque
2009-07-21 10:40 ` Georg Bauhaus
2009-07-21 10:46 ` Jean-Pierre Rosen
2009-07-21 11:33 ` xorque
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox