Subtype relation <:

Nov 22, 2013 at 5: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 12:54 PM
Hi Shaz,

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

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

Dec 6, 2013 at 9: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.

Dec 7, 2013 at 2: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?