ACSL (https://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language https://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Langu...) for C, which is based on

ACSL (https://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language https://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Langu...) for C, which is based on JML (https://en.wikipedia.org/wiki/Java_Modeling_Language https://en.wikipedia.org/wiki/Java_Modeling_Language) for Java, both use 'requires' for preconditions, 'ensures' for postconditions, and 'invariant' for invariants. Some invariants are also written as assertions ('assert').