File:Kadane run −2,1,−3,4,−1,2,1,−5,4.gif
From Wikimedia Commons, the free media repository
Jump to navigation
Jump to search
Size of this preview: 550 × 600 pixels. Other resolutions: 220 × 240 pixels | 440 × 480 pixels | 849 × 926 pixels.
Original file (849 × 926 pixels, file size: 10 KB, MIME type: image/gif)
File information
Structured data
Captions
Summary[edit]
DescriptionKadane run −2,1,−3,4,−1,2,1,−5,4.gif |
English: Execution trace of Kadane's algorithm on the array [−2,1,−3,4,−1,2,1,−5,4] |
Date | |
Source | Own work |
Author | Jochen Burghardt |
Source code[edit]
C / Frama-C source code |
---|
/*
* checked Sep 2023 with command
* frama-c -pp-annot -wp -wp-rte -wp-model Typed Kadane.c
* using frama-c 27.1 (Cobalt)
* and Alt-Ergo 2.4.3
*/
#include <limits.h>
//#define INT_MIN 0x80000000
/*@
// compute a[p]+...+a[q]
logic integer sum(integer p,integer q,int *a) =
( q < p
? 0
: q == p
? a[p]
: sum(p,q-1,a) + a[q]
);
*/
/*@
assigns \nothing;
ensures e1: a <= \result && b <= \result && (\result == a || \result == b);
*/
int max(
int a,
int b)
{
if (a < b)
return b;
else
return a;
}
///// Empty subarrays admitted ///////////////////////////////////////////////////////////////////////////////////////////
/*@
requires r1: 0 <= n;
requires r2: \valid(a + (0..n-1));
assigns \nothing;
ensures e1: \forall integer p,q; 0 <= p <= n && -1 <= q <= n-1 ==> sum(p,q,a) <= \result;
ensures e2: \exists integer p,q; 0 <= p <= n && -1 <= q <= n-1 && sum(p,q,a) == \result;
*/
int mss_empty(
int n,
const int a[n])
{
int best = 0;
int cur = 0;
int j;
/*@
loop assigns j, cur, best;
loop invariant i1: \forall integer p; 0 <= p <=j ==> sum(p,j-1,a) <= cur;
loop invariant i2: \exists integer p; 0 <= p <=j && sum(p,j-1,a) == cur;
loop invariant i3: \forall integer p,q; 0 <= p <=j && -1 <= q <= j-1 ==> sum(p,q ,a) <= best;
loop invariant i4: \exists integer p,q; 0 <= p <=j && -1 <= q <= j-1 && sum(p,q ,a) == best;
loop invariant i5: 0 <= j <= n;
loop invariant i6: 0 <= cur <= best;
loop variant n-j;
*/
for (j=0; j<n; ++j) {
//@ assert a1: sum(j+1,j,a) == 0;
cur = max(0,cur+a[j]);
best = max(best,cur);
}
return best;
}
///// No empty subarrays admitted ////////////////////////////////////////////////////////////////////////////////////////
/*@
requires r1: 0 < n;
requires r2: \valid(a + (0..n-1));
assigns \nothing;
ensures e1: \forall integer p,q; 0 <= p <= q <= n-1 ==> sum(p,q,a) <= \result;
ensures e2: \exists integer p,q; 0 <= p <= q <= n-1 && sum(p,q,a) == \result;
*/
int mss_nonempty(
int n,
const int a[n])
{
int best = INT_MIN;
int cur = 0;
int j;
/*@
loop assigns j, cur, best;
loop invariant i1: (\forall integer p; 0 <= p <= j-1 ==> sum(p,j-1,a) <= cur ) || ( j == 0 && cur == 0);
loop invariant i2: (\exists integer p; 0 <= p <= j-1 && sum(p,j-1,a) == cur ) || ( j == 0 && cur == 0);
loop invariant i3: (\forall integer p,q; 0 <= p <= q <= j-1 ==> sum(p,q ,a) <= best) || ( j == 0 && best == INT_MIN);
loop invariant i4: (\exists integer p,q; 0 <= p <= q <= j-1 && sum(p,q ,a) == best) || ( j == 0 && best == INT_MIN);
loop invariant i5: 0 <= j <= n;
loop variant n-j;
*/
for (j=0; j<n; ++j) {
//@ assert a1: a[j] == sum(j,j,a);
cur = max(a[j],cur+a[j]);
best = max(best,cur);
}
return best;
}
|
Licensing[edit]
I, the copyright holder of this work, hereby publish it under the following license:
This file is licensed under the Creative Commons Attribution-Share Alike 4.0 International license.
- You are free:
- to share – to copy, distribute and transmit the work
- to remix – to adapt the work
- Under the following conditions:
- attribution – You must give appropriate credit, provide a link to the license, and indicate if changes were made. You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
- share alike – If you remix, transform, or build upon the material, you must distribute your contributions under the same or compatible license as the original.
File history
Click on a date/time to view the file as it appeared at that time.
Date/Time | Thumbnail | Dimensions | User | Comment | |
---|---|---|---|---|---|
current | 21:25, 26 September 2019 | 849 × 926 (10 KB) | Jochen Burghardt (talk | contribs) | User created page with UploadWizard |
You cannot overwrite this file.
File usage on Commons
There are no pages that use this file.
File usage on other wikis
The following other wikis use this file:
- Usage on en.wikipedia.org