Praspel (PHP Realistic Annotation and Specification Language) is a formal specification language for PHP.