It is possible to write your own contract abbreviators with Code Contracts so I would hope such functionality gets added to the new language. The post does ment

It is possible to write your own contract abbreviators with Code Contracts so I would hope such functionality gets added to the new language. The post does mention however that object invariants are not supported so I do wonder how much Code Contracts are actually influencing it.