non-Void type system #723
Description
Rather than having to annotate /= Voids everywhere as we used to do in the pre-JML 5.4 days, we should introduce a non-null type system to BON and take advantage of it in BONc and Beetlz.
One idea is to follow Spec#'s lead and annotate classnames with markers to indicate if they are nullable or non-null.
E.g.,
{{{
o: ANY!
p: ANY
}}}
means that o is non-Void and p can be Void.
Alternatively, we could follow the Eiffel solution and declare non-Void references as "expanded" and then just reuse the type checking rules for Eiffel for BON.