Re: Question about jStar

[Radu Grigore]

You can use the spec
remove(...) { lspe(head, nil()) } { lspe($ret_v1, nil()) };
with the attached logic, which is less than half the original one. I
hope it is sound.

Just as in the Java's library [1], it makes more sense for the method
LinkedList.remove to have a different signature.
void remove(String key);

regards,
radu

[1] http://goo.gl/ssAFc

2011/2/28 Yifan Yao <yyf8...@gmail.com>:
> Dear Grigore,
>
> I'm tring to implement some verification for the linkedlist. I wrote a
> method that remove the certain node from the linkedlist.
> NodeLL remove(NodeLL head, NodeLL key){
> NodeLL h = head;
> NodeLL s = key;
> if (h != null) {
> if(h == s){
> NodeLL t;
> t = h.next;
> h.next = null;
> return t;
> }
> else{
> h.next = remove(h.next, s);
> return h;
> }
> }
> else
> return null;
> }
>
> like this. But I don't know how to write the spec....and do i need more
> logic rule to support? I don't know how to deal with the
> parameter......If you see this email, can you help me. Thank you so much.
>
> Cheers, Yifan Yao.
>