Primer

V primeru zaporedj.c imamo za funkcijo sestej_zaporedje1 naslednjo pogodbo:

/* Desc:    Funkcija sesteje stevilo_clenov aritmeticnega
            zaporedja, ki je definiran z zacetnim clenom
            zacetni_clen in korakom korak.
   Parms:   zacetni_clen - zacetni clen zaporedja (po vrednosti)
            korak - razlika med zaporednima clenoma zaporedja (po
            vrednosti)
            stevilo_clenov - stevilo clenov zaporedja, ki jih
            bomo sesteli (po vrednosti)
   Result:  Sum(ai: ai = zacetni_clen + (i * korak),
                0 <= i < stevilo_clenov)
   Pre:     (RESULT IN int) AND (stevilo_clenov >= 0)
   Post:    -
*/

Na nasem podrocju si lahko ogledate drugo inacico pogodbe, pri kateri sta spremenjna clena ,,Result'' in ,,Post``.