Is it possible to write an ensures that refers to both the original and
final value of an array. For exampe, if one makes a function update ar i
v, one might want to write an ensures that indicates that only the ith
element of the array is updated. All of the others remain unchanged.
thanks,
jul
Le 27/02/2018 à 08:18, Julia Lawall a écrit :
Is it possible to write an ensures that refers to both the original and
final value of an array. For exampe, if one makes a function update ar i
v, one might want to write an ensures that indicates that only the ith
element of the array is updated.
On Tue, 27 Feb 2018, Guillaume Melquiond wrote:
> Le 27/02/2018 à 08:18, Julia Lawall a écrit :
> > Is it possible to write an ensures that refers to both the original and
> > final value of an array. For exampe, if one makes a function update ar i
> > v, one might want to write an ensures that
Here is another typical usage, say for the swap function:
let swap (a:array 'a) (i:int) (j:int) : unit
requires { 0 <= i < a.length /\ 0 <= j < a.length }
writes { a }
ensures { a[i] = (old a)[j] }
ensures { a[j] = (old a)[i] }
ensures { forall k. 0 <= k < a.length /\
On Tue, 27 Feb 2018, Claude Marché wrote:
>
> Here is another typical usage, say for the swap function:
>
>
> let swap (a:array 'a) (i:int) (j:int) : unit
> requires { 0 <= i < a.length /\ 0 <= j < a.length }
> writes { a }
> ensures { a[i] = (old a)[j] }
> ensures { a[j] =
On Tue, 27 Feb 2018, Claude Marché wrote:
>
> Here is another typical usage, say for the swap function:
>
>
> let swap (a:array 'a) (i:int) (j:int) : unit
> requires { 0 <= i < a.length /\ 0 <= j < a.length }
> writes { a }
> ensures { a[i] = (old a)[j] }
> ensures { a[j] =
On Thu, Mar 8, 2018 at 11:09 AM Julia Lawall wrote:
>
>
> On Tue, 27 Feb 2018, Claude Marché wrote:
>
> >
> > Here is another typical usage, say for the swap function:
> >
> >
> > let swap (a:array 'a) (i:int) (j:int) : unit
> > requires { 0 <= i < a.length /\ 0 <= j < a.length }
> > wr
On Thu, 8 Mar 2018, Alix TRIEU wrote:
> On Thu, Mar 8, 2018 at 11:09 AM Julia Lawall wrote:
>
>
> On Tue, 27 Feb 2018, Claude Marché wrote:
>
> >
> > Here is another typical usage, say for the swap function:
> >
> >
> > let swap (a:array 'a) (i:int) (j:int)
