Skip to content

Instantly share code, notes, and snippets.

@codelion

codelion/listlength.c

Last active June 14, 2017 07:21
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save codelion/ab5e055e06d2fc95087190b284da7266 to your computer and use it in GitHub Desktop.
Save codelion/ab5e055e06d2fc95087190b284da7266 to your computer and use it in GitHub Desktop.
Download ZIP
Verifying shape property
Raw
listlength.c
struct node{
int val;
struct node* next;
};
/*@
list<> == self=null or self::node<_,q> * q::list<>;
*/
int length(struct node* p)
/*@
requires p::list<>
ensures p::list<>;
*/
{
if (p==NULL) return 0;
else return 1 + length(p->next);
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment