A Language Framework for Expressing Checkable Properties of Dynamic Software