形式化方法的问题

学了形式化方法这么课，是有很大的启发的。不管对测试还是开发.但是也有不少问题.于是写了下面的感言：

形式化是因规范化，拒绝二义性而产生的。形式化方法希望用技术的手段提高软件的可靠性，安全性,
减少程序设计中的错误。希望机器可以理解形式化语言，并可以自动的检测程序中的错误。
形式化语言是基于数学的语言，从而可以避免二义性，将语言严格化，规范化。
软件需求等自然语言的描述方法，常常造成软件设计，软件开发的不一致性和不正确性。
但是，形式化方法也不能够代替现有的测试方法，和其他工程学管理方法。
另外因为使用形式化方法也需要一定的技巧，所以使用形式化方法所做的规约的正确性可靠性有时只能靠经验和手工验证去保证。例如人羊过河问题。最后的SPEC是使用EF
还是使用 AF，究竟是模型错误还是规约错误，这样的问题很难让机器做出回答。
或许这是形式化方法学之外的范畴。我个人认为不应该使用一种高技巧的方法来保证程序的正确性和可靠性。
虽然它已经成功的运用在软件规约，协议验证和硬件设计等方面，但是距离像java那样普及，尚待时日。