Skip to content

Commit

Permalink
add more examples
Browse files Browse the repository at this point in the history
  • Loading branch information
@elaustell
elaustell committed Jul 29, 2024
1 parent 064a1a7 commit 4fd14bf
Show file tree
Hide file tree
Showing 2 changed files with 152 additions and 50 deletions.
2 changes: 1 addition & 1 deletion src/examples/Dbl_Queue/lemmas.c
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#include "./predicates.c"
// #include "./predicates.c"

void Own_Inner_fwds_append_lemma(struct node *front, struct node *second_last, struct node *last)
/*@
Expand Down
200 changes: 151 additions & 49 deletions src/examples/Dbl_Queue/main.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,81 +12,183 @@ int main()


push_front(q, 1);
/*@ split_case(is_null(q)); @*/
/*@ split_case(is_null(q->front)); @*/
/*@ split_case(is_null(q->back)); @*/
/*@ split_case(ptr_eq(q->front, q->back)); @*/
/*@ assert(ptr_eq(q->front, q->back)); @*/
/*@ assert(q->front->data == 1i32); @*/
/*@ assert(q->back->data == 1i32); @*/
// /*@ split_case(is_null(q)); @*/
// /*@ split_case(is_null(q->front)); @*/
// /*@ split_case(is_null(q->back)); @*/
// /*@ split_case(ptr_eq(q->front, q->back)); @*/
// /*@ assert(ptr_eq(q->front, q->back)); @*/
// /*@ assert(q->front->data == 1i32); @*/
// /*@ assert(q->back->data == 1i32); @*/


Dbl_Queue_Fwd_At_eq_Bwd_lemma(q);
/*@ split_case(is_null(q)); @*/
/*@ split_case(is_null(q->front)); @*/
/*@ split_case(is_null(q->back)); @*/
// Dbl_Queue_Fwd_At_eq_Bwd_lemma(q);
// /*@ split_case(is_null(q)); @*/
// /*@ split_case(is_null(q->front)); @*/
// /*@ split_case(is_null(q->back)); @*/

/*@ split_case(ptr_eq(q->front, q->back)); @*/
/*@ assert(ptr_eq(q->front, q->back)); @*/
// /*@ assert(q->front->data == 1i32); @*/
// /*@ assert(q->back->data == 1i32); @*/
// /*@ split_case(ptr_eq(q->front, q->back)); @*/
// /*@ assert(ptr_eq(q->front, q->back)); @*/
// // /*@ assert(q->front->data == 1i32); @*/
// // /*@ assert(q->back->data == 1i32); @*/


push_back(q, 2);
/*@ split_case(is_null(q->front)); @*/
/*@ split_case(ptr_eq(q->front, q->back)); @*/
// /*@ assert(q->front->data == 1i32); @*/
// /*@ assert(q->back->data == 2i32); @*/
/*@ assert(!ptr_eq(q->front, q->back)); @*/
/*@ split_case(ptr_eq(q->back->prev, q->front)); @*/
/*@ assert(ptr_eq(q->back->prev, q->front)); @*/
// /*@ assert(q->front->data == 1i32); @*/
// /*@ assert(q->back->data == 2i32); @*/
// push_back(q, 2);
// /*@ split_case(is_null(q->front)); @*/
// /*@ split_case(ptr_eq(q->front, q->back)); @*/
// // /*@ assert(q->front->data == 1i32); @*/
// // /*@ assert(q->back->data == 2i32); @*/
// /*@ assert(!ptr_eq(q->front, q->back)); @*/
// /*@ split_case(ptr_eq(q->back->prev, q->front)); @*/
// /*@ assert(ptr_eq(q->back->prev, q->front)); @*/
// // /*@ assert(q->front->data == 1i32); @*/
// // /*@ assert(q->back->data == 2i32); @*/

Dbl_Queue_Bwd_At_eq_Fwd_lemma(q);
push_front(q, 3);
// Dbl_Queue_Bwd_At_eq_Fwd_lemma(q);
// push_front(q, 3);


/*@ split_case(is_null(q)); @*/
/*@ split_case(is_null(q->front)); @*/
/*@ split_case(ptr_eq(q->front, q->back)); @*/
/*@ assert(q->front->data == 3i32); @*/
// /*@ assert(q->front->next->data == 1i32); @*/
/*@ assert(q->back->data == 2i32); @*/
// /*@ split_case(is_null(q)); @*/
// /*@ split_case(is_null(q->front)); @*/
// /*@ split_case(ptr_eq(q->front, q->back)); @*/
// /*@ assert(q->front->data == 3i32); @*/
// // /*@ assert(q->front->next->data == 1i32); @*/
// /*@ assert(q->back->data == 2i32); @*/

/*@ split_case(ptr_eq(q->front->next, q->back)); @*/
/*@ split_case(ptr_eq(q->front->next->next, q->back)); @*/
/*@ split_case(ptr_eq(q->back->prev, q->front)); @*/
// /*@ split_case(ptr_eq(q->front->next, q->back)); @*/
// /*@ split_case(ptr_eq(q->front->next->next, q->back)); @*/
// /*@ split_case(ptr_eq(q->back->prev, q->front)); @*/




int three = pop_front(q);
// int three = pop_front(q);


/*@ split_case(is_null(q->front)); @*/
/*@ split_case(is_null(q->back)); @*/
// /*@ split_case(is_null(q->front)); @*/
// /*@ split_case(is_null(q->back)); @*/

// /*@ split_case(ptr_eq(q->front, q->back)); @*/

// /*@ assert(!is_null(q)); @*/
// /*@ assert(!is_null(q->front)); @*/
// /*@ assert(!is_null(q->back)); @*/
// /*@ assert(q->front->data == 3i32); @*/
// /*@ assert(q->back->data == 2i32); @*/

// Dbl_Queue_Fwd_At_eq_Bwd_lemma(q);
// /*@ split_case(is_null(q)); @*/
// /*@ split_case(is_null(q->front)); @*/
// /*@ split_case(is_null(q->back)); @*/

// /*@ split_case(ptr_eq(q->front, q->back)); @*/

// /*@ unfold rev(Seq_Nil{}); @*/
// // /*@ assert(!is_null(q->front)); @*/


// int two = pop_back(q);



int one = pop_front(q);
/*@ assert(one == 1i32); @*/
/*@ split_case(is_null(q->front)); @*/
/*@ split_case(ptr_eq(q->front, q->back)); @*/
free_dbl_queue(q);
}

/*@ assert(!is_null(q)); @*/
/*@ assert(!is_null(q->front)); @*/
/*@ assert(!is_null(q->back)); @*/
/*@ assert(q->front->data == 3i32); @*/
/*@ assert(q->back->data == 2i32); @*/
void ex_front()
{
struct dbl_queue *q = empty_dbl_queue();
push_front(q, 1);

int one = pop_front(q);
/*@ assert(one == 1i32); @*/

Dbl_Queue_Fwd_At_eq_Bwd_lemma(q);
/*@ split_case(is_null(q)); @*/
/*@ split_case(is_null(q->front)); @*/
/*@ split_case(ptr_eq(q->front, q->back)); @*/
free_dbl_queue(q);
}

void ex_back()
{
struct dbl_queue *q = empty_dbl_queue();

/*@ split_case(is_null(q->back)); @*/
/*@ split_case(ptr_eq(q->front, q->back)); @*/

push_back(q, 1);

int one = pop_back(q);
/*@ assert(one == 1i32); @*/

/*@ split_case(is_null(q->front)); @*/
/*@ split_case(ptr_eq(q->front, q->back)); @*/

free_dbl_queue(q);
}

// void ex_switch()
// {
// struct dbl_queue *q = empty_dbl_queue();
// push_front(q, 1);
// /*@ split_case(is_null(q->front)); @*/
// /*@ split_case(is_null(q->back)); @*/
// /*@ split_case(ptr_eq(q->front, q->back)); @*/
// /*@ split_case(ptr_eq(q->front->next, q->back)); @*/
// /*@ split_case(is_null(q)); @*/
// /*@ unfold rev(Seq_Nil{}); @*/
// /*@ assert(q->front->data == 1i32); @*/
// /*@ assert(!is_null(q->front)); @*/
// /*@ assert(!is_null(q->back)); @*/

// Dbl_Queue_Fwd_At_eq_Bwd_lemma(q);
// /*@ assert(!is_null(q->front)); @*/
// /*@ assert(!is_null(q->back)); @*/

// /*@ assert(q->back->data == 1i32); @*/

// /*@ unfold rev(Seq_Cons{head: 1i32, tail: Seq_Nil{}}); @*/
// /*@ unfold rev(Seq_Nil{}); @*/
// /*@ split_case(is_null(q)); @*/
// /*@ split_case(is_null(q->front)); @*/
// /*@ split_case(is_null(q->back)); @*/
// // /*@ split_case(ptr_eq(q->front, q->back->prev)); @*/


// /*@ split_case(ptr_eq(q->front, q->back)); @*/
// int one = pop_back(q);
// /*@ assert(one == 1i32); @*/

// /*@ split_case(is_null(q->front)); @*/
// /*@ split_case(ptr_eq(q->front, q->back)); @*/
// free_dbl_queue(q);
// }

void ex_switch()
{
struct dbl_queue *q = empty_dbl_queue();
push_front(q, 1);
Dbl_Queue_Fwd_At_eq_Bwd_lemma(q);
push_back(q, 2);
int two = pop_back(q);
int one = pop_back(q);
/*@ assert(one == 1i32); @*/
/*@ assert(two == 2i32); @*/

/*@ unfold rev(Seq_Nil{}); @*/
// /*@ assert(!is_null(q->front)); @*/
/*@ split_case(is_null(q->front)); @*/
/*@ split_case(ptr_eq(q->front, q->back)); @*/
free_dbl_queue(q);
}


int two = pop_back(q);
void foo()
{
struct dbl_queue *q = empty_dbl_queue();
push_front(q, 1);

Dbl_Queue_Fwd_At_eq_Bwd_lemma(q);

int one = pop_back(q);
free_dbl_queue(q);
}

0 comments on commit 4fd14bf

Please sign in to comment.