Abstract. A concept of annotations for rendering procedural aspects of Prolog is presented, built around wellknown procedural concepts of Standard Prolog. Annotations describe properties of predicates. Such properties can be pre or post conditions, which must hold true when a predicate is called or exited, respectively. Our concept transcends pre/post conditions: we introduce two more kinds of annotations, fail and redo annotations, hence incorporating a whole model of Prolog execution into our language. This enables natural rendering of many procedural properties of Prolog which cannot be expressed with only pre/post conditions. There are four more novelties in our approach. First, any annotation can be “narrowed down” to a subset of calls, via templates and contexts, giving much more flexible assertions. Notably the novel idea of calling context adds significant expressive power, as a bridge towards program-point assertions. The annotations are defined simply as Prolog goals, ...