Na ferramenta de prova que é usada nesta disciplina é utilizada uma linguagem para especificar programas concorrentes designada Simple Programming Language (SPL). Nesta secção iremos abordar a sintaxe (e a semântica ?!) desta linguagem.