Subtype relation <:

Coordinator
Nov 22, 2013 at 4:54 PM
I am wondering if any client of Boogie uses the subtype relation <: available in Boogie. I believe it was added for encoding Spec# a long time ago. I am considering deleting it if nobody uses it.
Dec 4, 2013 at 11:54 AM
Hi Shaz,

Spec# still uses <:, so it would be good to keep it.


Thanks,
Peter
Coordinator
Dec 5, 2013 at 10:46 PM
Doesn't SscBoogie use a particular binary version of Boogie (from 2010)?

Rustan
Developer
Dec 6, 2013 at 8:11 PM
Yes, SscBoogie currently uses a Boogie snapshot from early 2011. I remember that I also used the subtype relation for encoding the inheritance hierarchy in my Boogie encoding for Scala, but I'm not sure if there are more verifiers (e.g., AutoProof) that are doing the same.

Valentin
Dec 7, 2013 at 1:45 PM
Yes, AutoProof uses it, so we would appreciate if you leave it. That said, I guess it can also be encoded as a function with partial order axioms. Or does it use something special from Z3?