The Free On-line Dictionary of Computing (19 January 2023):

SPARK Annotation Language

    (SAL) ICL, Ltd.  Used in the verification of
   SPARK programs against Z specifications.

   (1994-12-08)