requires and ensures for properties and methods
also properties now have the no-null flair