We propose to allow specifying precondition and postcondition assertions on virtual functions, in the same way they can already be specified on non-virtual functions: