From 1c39545f975e266ac4e3e4f46e3b555edc1d8d0b Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 26 Oct 2026 12:19:38 +0000 Subject: [PATCH 1/3] Add lowerbounds for iterated separating conjunctions --- src/exercises/array_init.c | 6 +++--- src/exercises/array_init_rev.c | 8 ++++---- src/exercises/array_load.c | 6 +++--- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/exercises/array_init.c b/src/exercises/array_init.c index a4755894..fcabe95f 100644 --- a/src/exercises/array_init.c +++ b/src/exercises/array_init.c @@ -1,14 +1,14 @@ void array_init (char *p, unsigned int n) -/*@ requires take A = each(integer i; i < n) { +/*@ requires take A = each(integer i; 0 <= i && i < n) { RW( array_shift(p, i)) }; - ensures take A_post = each(integer i; i < n) { + ensures take A_post = each(integer i; 0 <= i && i < n) { RW( array_shift(p, i)) }; @*/ { unsigned int j = 0; while (j < n) /* --BEGIN-- */ - /*@ inv take Ai = each(integer i; i < n) { + /*@ inv take Ai = each(integer i; 0 <= i && i < n) { RW( array_shift(p, i)) }; {p} unchanged; {n} unchanged; diff --git a/src/exercises/array_init_rev.c b/src/exercises/array_init_rev.c index 03ede4cd..b3c1e2c9 100644 --- a/src/exercises/array_init_rev.c +++ b/src/exercises/array_init_rev.c @@ -1,16 +1,16 @@ void array_init_rev (char *p, unsigned int n) -/*@ requires take A = each(integer i; i < n) { +/*@ requires take A = each(integer i; 0 <= i && i < n) { RW( array_shift(p, i)) }; - ensures take A_post = each(integer i; i < n) { + ensures take A_post = each(integer i; 0 <= i && i < n) { RW( array_shift(p, i)) }; @*/ { unsigned int j = 0; while (j < n) /* --BEGIN-- */ - /*@ inv take Al = each(integer i; i < n-j) { + /*@ inv take Al = each(integer i; 0 <= i && i < n-j) { RW( array_shift(p, i)) }; - take Ar = each(integer i; n-j <= i && i < n) { + take Ar = each(integer i; n-j <= i && i < n) { RW( array_shift(p, i)) }; {p} unchanged; {n} unchanged; j <= n; diff --git a/src/exercises/array_load.c b/src/exercises/array_load.c index f1efd5cf..0e919f80 100644 --- a/src/exercises/array_load.c +++ b/src/exercises/array_load.c @@ -1,8 +1,8 @@ unsigned int read (unsigned int *p, unsigned int n, unsigned int i) -/*@ requires take A = each(integer j; j < n) +/*@ requires take A = each(integer j; 0 <= j && j < n) { RW(array_shift(p,j)) }; - i < n; - ensures take A_post = each(integer j; j < n) + i < n; + ensures take A_post = each(integer j; 0 <= j && j < n) { RW(array_shift(p,j)) }; return == A[i]; @*/ From a9604e536b8a6655aa02c9cabfc12157889a6f4c Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 26 Oct 2026 12:35:50 +0000 Subject: [PATCH 2/3] Fix unnecessary diff --- src/exercises/array_load.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/exercises/array_load.c b/src/exercises/array_load.c index 0e919f80..9f7705e7 100644 --- a/src/exercises/array_load.c +++ b/src/exercises/array_load.c @@ -1,7 +1,7 @@ unsigned int read (unsigned int *p, unsigned int n, unsigned int i) /*@ requires take A = each(integer j; 0 <= j && j < n) { RW(array_shift(p,j)) }; - i < n; + i < n; ensures take A_post = each(integer j; 0 <= j && j < n) { RW(array_shift(p,j)) }; return == A[i]; From 43c35a49e1bf8275ee3bf968f9c7d0b4f792cc00 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 26 Oct 2026 12:37:49 +0000 Subject: [PATCH 3/3] Fix another unnecessary diff --- src/exercises/array_init_rev.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/exercises/array_init_rev.c b/src/exercises/array_init_rev.c index b3c1e2c9..cde7086e 100644 --- a/src/exercises/array_init_rev.c +++ b/src/exercises/array_init_rev.c @@ -10,7 +10,7 @@ void array_init_rev (char *p, unsigned int n) /* --BEGIN-- */ /*@ inv take Al = each(integer i; 0 <= i && i < n-j) { RW( array_shift(p, i)) }; - take Ar = each(integer i; n-j <= i && i < n) { + take Ar = each(integer i; n-j <= i && i < n) { RW( array_shift(p, i)) }; {p} unchanged; {n} unchanged; j <= n;