From bd52075c222b761ac4bc79cec14ea1f2ceb95b8b Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Tue, 31 Jan 2017 22:25:59 +0100 Subject: [PATCH] ascii art --- plugins/python/examples/sort.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/plugins/python/examples/sort.py b/plugins/python/examples/sort.py index 8f88730e4..e6f70b7b3 100644 --- a/plugins/python/examples/sort.py +++ b/plugins/python/examples/sort.py @@ -1,3 +1,4 @@ + from random import randint n = 42 @@ -17,10 +18,10 @@ while m < len(a): k = m while k > 0 and a[k-1] > x: #@ invariant 0 <= k <= m - #@ invariant forall j. k < j <= m -> x < a[j] - #@ invariant forall i,j. k < i <= j <= m -> a[i] <= a[j] - #@ invariant forall i,j. 0 <= i <= j < k -> a[i] <= a[j] - #@ invariant forall i,j. 0 <= i < k < j <= m -> a[i] <= a[j] + #@ invariant forall i,j. 0 <= i <= j < k -> a[i] <= a[j] + #@ invariant forall i,j. 0 <= i < k < j <= m -> a[i] <= a[j] + #@ invariant forall i,j. k < i <= j <= m -> a[i] <= a[j] + #@ invariant forall j. k < j <= m -> x < a[j] #@ variant k a[k] = a[k-1] k = k - 1 -- GitLab