formal specification: In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools.[1][2] These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.

在计算机科学中，formal specification是一种基于数学的辅助系统和软件实现的技术。人们可以使用它来描述系统，分析系统的行为，或者在设计阶段通过一些缜密有效的工具使用它来验证关键点。之所以这里有formal的意思，是因为他们有着语法，在某些领域有着自己的语义。

formal speicification例子之一就是JML，Java Model Language，Java建模语言

就其本身而言，程序符号（代码）只是说明了如何作某些功能，但并没有说明我们要做什么事情。如果在开始开发之前能够达成我们要做什么事情的话就会很有帮助。但是Java并没有提供此种支持
JML添加注解annotations到Java代码中

java concurrency 笔记