Introducing 

Prezi AI.

Your new presentation assistant.

Refine, enhance, and tailor your content, source relevant images, and edit visuals quicker than ever before.

Loading…
Transcript

Implementacja

Równoważność programów

Wstęp

Wyniki

Podsumowanie

Zadanie

Codility

Kontrprzykład

Programy

Założenia

Sędzia

dobre (100/100)

Ocenianie

T

Program

int add(int a, int b) {

return a + b;

}

50/100

?

Rozwiązania

void check(int r1, int r2)

{

assert(r1 == r2);

}

Fałszywy alarm

void assumptions(int a, int b)

{

__CPROVER_assume(a > 0);

__CPROVER_assume(b > 0);

}

int add(int a, int b) {

while (--b)

++a;

return a;

}

złe (np. 50/100)

=

Program 1

Program 2

Brak kontrprzykładu

Podobne zadanie

Program 1

Program 2

  • narzędzia

  • serwisy Codility

  • pokazowa strona WWW

  • praca magisterska

  • ulepszenia

NIE

TAK

Sędzia

+

kontrprzykład

Program 1

Program 2

Scalenie

int add1() ...

int add2() ...

int main()

{

int a = nondet_int();

int b = nondet_int();

assumptions(a, b);

int r1 = add1(a, b);

int r2 = add2(a, b);

check(r1, r2);

}

Proste różnice

w semantyce

int equi ( int A[], int n ) {

if(n<=0)

return -1;

int64_t backSum = 0, forSum = 0;

int i;

for(i=0; i<n; i++)

backSum += A[i];

for(i=0; i<n; i++)

{

backSum -= A[i];

if(backSum == forSum)

return i;

forSum += A[i];

}

return -1;

}

int maxRS ( int A[], int n ) {

int best=0, current=0, i, begin=0, ii=0;

for (i=0;i<n;i++){

if (A[i]<A[i+1]){

current = current +1;

}else{

if (current>best){

best=current;

ii=begin;

current=0;

begin=i;

}else{

current=0;

begin=i+1;

}

}

}

return ii;

}

złośliwość

vs

przypadek

[[-2147483648, -2147483648, 4194304]]

Program C

file source.c: Parsing

Converting

Type-checking source

Generating GOTO Program

...

Program

GOTO

...

size of program expression: 414 assignments

simple slicing removed 5 assignments

...

{-213} i@1#20 == (\guard#24 && \guard#25 && \guard#26 &&

\guard#27 && \guard#28 && !\guard#29 ? i@1#12 : i@1#19)

{-214} sum_left@1#11 == (\guard#24 && \guard#25 && \guard#26 &&

\guard#27 && \guard#28 && !\guard#29 ? sum_left@1#3 : sum_left@1#10)

...

CBMC

Formuła logiczna

?

...

Passing problem to propositional reduction

Running propositional reduction

Solving with MiniSAT2 without simplifier

60281 variables, 220208 clauses

Verified 209725 original clauses.

SAT checker: negated claim is SATISFIABLE, i.e., does not hold

Runtime decision procedure: 0.691s

...

State 47 file source.c line 94 function equi thread 0

----------------------------------------------------

source::equi::1::i=1 (00000000000000000000000000000001)

State 49 file source.c line 95 function equi thread 0

----------------------------------------------------

source::equi::1::right=3242196992 (0000000000000000000000000000000011000001010000000000000000000000)

State 50 file source.c line 94 function equi thread 0

----------------------------------------------------

source::equi::1::i=2 (00000000000000000000000000000010)

State 53 file source.c line 95 function equi thread 0

----------------------------------------------------

source::equi::1::right=4261474304 (0000000000000000000000000000000011111110000000001111000000000000)

State 54 file source.c line 94 function equi thread 0

----------------------------------------------------

source::equi::1::i=3 (00000000000000000000000000000011)

State 59 file source.c line 99 function equi thread 0

----------------------------------------------------

source::equi::1::i=1 (00000000000000000000000000000001)

State 61 file source.c line 100 function equi thread 0

----------------------------------------------------

source::equi::1::left=1052770304 (0000000000000000000000000000000000111110110000000000000000000000)

State 62 file source.c line 101 function equi thread 0

----------------------------------------------------

source::equi::1::right=1019277312 (0000000000000000000000000000000000111100110000001111000000000000)

Nieznane

funkcje

int equi( int A[], int n )

{

if( n <= 0 )

return -1;

int total = sum( A, n );

double lhs = 0.0, rhs = total;

unsigned int i;

for( i = 0; i < n; ++i )

{

rhs -= A[i];

if( fabs(rhs - lhs) < 1e-6 )

return i;

lhs += A[i];

}

return -1;

}

Spełnialność ?

int equi ( int A[], int n ) {

if (n <= 0)

return -1;

int i,j,k;

unsigned long long left = 0;

unsigned long long right = 0;

for (i = 1 ; i < n ; ++i) {

right += A[i];

}

if (left == right)

return 0;

for (i = 1; i < n; ++i) {

left += A[i - 1];

right -= A[i];

if (left == right)

return i;

}

return -1;

}

Kontrprzykład

(traceback)

Counterexample:

State 2 file source.c line 11 thread 0

----------------------------------------------------

arr=NULL

State 3 file source.c line 12 thread 0

----------------------------------------------------

n=0 (00000000000000000000000000000000)

State 4 file /usr/include/stdio.h line 165 thread 0

----------------------------------------------------

stdin=NULL

State 5 file /usr/include/stdio.h line 166 thread 0

----------------------------------------------------

stdout=NULL

State 6 file /usr/include/stdio.h line 167 thread 0

----------------------------------------------------

stderr=NULL

State 7 file /usr/include/bits/sys_errlist.h line 27 thread 0

----------------------------------------------------

sys_nerr=0 (00000000000000000000000000000000)

State 8 file line 19 thread 0

----------------------------------------------------

__CPROVER_alloc={ [3]=FALSE }

State 9 file line 20 thread 0

----------------------------------------------------

__CPROVER_alloc_size={ [3]=0 }

State 10 file line 29 thread 0

----------------------------------------------------

__CPROVER_rounding_mode=0 (00000000000000000000000000000000)

State 13 thread 0

----------------------------------------------------

c::argv'=(assignment removed)

State 17 file source.c line 23 function main thread 0

----------------------------------------------------

n=1073741826 (01000000000000000000000000000010)

State 19 file source.c line 25 function main thread 0

----------------------------------------------------

c::main::$tmp::return_value_malloc$1=&dynamic_1_array[0]

State 21 file source.c line 25 function main thread 0

----------------------------------------------------

__CPROVER_alloc_size={ [3]=1073741826 }

State 22 file source.c line 25 function main thread 0

----------------------------------------------------

__CPROVER_alloc={ [3]=TRUE }

State 23 file source.c line 25 function main thread 0

----------------------------------------------------

arr=&dynamic_1_array[0]

State 24 file source.c line 28 function main thread 0

----------------------------------------------------

source::main::1::1::i=0 (00000000000000000000000000000000)

0

State 27 file source.c line 28 function main thread 0

----------------------------------------------------

source::main::1::1::i=1 (00000000000000000000000000000001)

0

State 31 file source.c line 28 function main thread 0

----------------------------------------------------

source::main::1::1::i=2 (00000000000000000000000000000010)

0

State 35 file source.c line 28 function main thread 0

----------------------------------------------------

source::main::1::1::i=3 (00000000000000000000000000000011)

402653444

State 39 file source.c line 28 function main thread 0

----------------------------------------------------

source::main::1::1::i=4 (00000000000000000000000000000100)

Violated property:

file source.c line 28 function main

unwinding assertion loop 0

VERIFICATION FAILED

int equi ( int A[], int n ) {

long long i;

long long j;

long long a, b;

a = 0;

b = 0;

for(i = 0; i < n; i++) {

b = 0;

for(j = i + 1; j < n; j++)

b += A[j];

if(a == b)

return i;

a += A[i];

}

return -1;

}

int equi ( int A[], int n ) {

float sum = 0;

int i = 0;

for (i = 0; i < n; i++)

{

sum += A[i];

}

float left = 0;

float right = sum;

float val = 0;

i = 0;

for (i = 0; i < n; i++)

{

val = A[i];

right = right - val;

if (left == right)

return i;

else

left = left + val;

}

return -1;

}

Słaba

wydajność

  • gdb ? printf ?

Błędy

parsowania

int equi ( int A[], int n ) {

int sumlow(int A[], int k){

int i, sumaL = 0;

for(i = 0; i < k; ++i) sumaL+=A[i];

return sumaL;

}

int sumhi(int A[], int n, int k){

int i, sumaH = 0;

for(i = k; i < n; ++i) sumaH+=A[i];

return sumaH;

}

int j=0;

for(j=0; j < n; j++){

if (sumlow(A, j) == sumhi(A,n,j+1)) return j;

}

return -1;

}

Niepotwierdzony kontrprzykład

[-268435456, 8]

Kontrprzykład

int equi ( int A[], int n ) {

long long int low = 0;

long long int high = 0;

int i;

for(i=0; i<n; ++i){

high+=A[i];

}

for(i=0; i<n; ++i){

if(low + A[i] == high){

return i;

}

low += 2*A[i];

}

return -1;

}

234 (8.1%)

a = 34, b = 2

Niepotwierdzony

kontrprzykład

34 (5.8%)

[2014818472, 275785409, 2014818472]

Brak

kontrprzykładu

Kontrprzykład

int maxRS ( int A[], int n ) {

int count=1, ii=0, pi=0, i, countp=0;

if (n==0)

return -1;

for (i=1;i<n;i++) {

if (A[i]>A[i-1])

count++;

else {

if (countp<count) {

pi=ii;

countp=count;

}

count=0;

ii=i;

}

}

return (count>=countp)?ii:pi;

}

int add(int a, int b) {

return a + b;

}

int add(int a, int b) {

while (--b)

++a;

return a;

}

105 (3.6%)

[20, 16, 1024, 0]

35 (5.9%)

35

36

DOWÓD NIERÓWNOWAŻNOŚCI

Złe rozwiązania

Dobre rozwiązania

522 (88.3%)

2542 (88.2%)

Brak kontrprzykładu

Kontrprzykład

Brak wydajności

Błędy

parsowania

Poprawność

int equi ( int A[], int n ) {

int x;

long long left=0,right=0;

for(x = 0; x < n; right += (long long)A[x++]);

for(x = 0; x < n; x++) {

right -= (long long)A[x];

if(left == right)

return x;

left += (long long)A[x];

}

return left != right ? -1 : (n-1);

}

int equi ( int A[], int n ) {

long long lsum = 0;

long long rsum = 0;

int i;

for ( i=0 ; i<n ; i++)

rsum+= A[i];

for ( i=0 ; i<n ; i++)

{

if (i != 0)

lsum += A[i-1];

rsum -= A[i];

if ( lsum==rsum )

return i;

}

return -1;

}

[-12, 12]

Learn more about creating dynamic, engaging presentations with Prezi