rems-project / cn-tutorial

7 stars 8 forks source link

Binary Search Tree Data Structure #57

Closed MedranoApol closed 1 week ago

bcpierce00 commented 1 month ago

This looks very nice, Apol.

I think it would make a good "optional extended exercise" in the tutorial, for people that want to practice their simple-functional-specification chops. I suggest adding some BEGIN/END annotations so that we can generate a version that is just the C code with little to no CN. (This may involve reorganizing the files a little, since at the moment some of them contain only CN code.)

septract commented 2 weeks ago

What else is needed to merge this?

bcpierce00 commented 1 week ago

On a more careful reading, this is a good start toward a BST example, but it its definition of what it means to be a BST is not quite correct. I'm going to put it on the side for now.

bcpierce00 commented 1 week ago

(I'll keep the files in an /underconstruction directory, though, in case anybody wants to come back to it later.)