The key to getting people to buy into any methods or methodologies is to show them how it solves problems they are having. If they can see it will make their lives better you have a much improved chance of getting them to adopt the techniques.
And if you can't show them that, perhaps you wanted to adopt the methods based on philosophy rather than practicality. Unless the others share your philosophy then you're not going to get anywhere. And perhaps you shouldn't.
Over the decades there have been a great many methodologies. Newer ones always address the shortcomings of the old ones, yet projects still get in trouble and fail. Why? Because the rock stars that come up with new methodologies are rock stars, and have made a new methodology precisely because they understand the underlying issues and how to apply them. Those who come after tend to blindly follow the recipe, and it doesn't work so well.
So I think the best thing is to teach about the underlying problems and then show how various methods attempt to deal with those problems. The differences in companies, projects, and teams is so great that no one methodology can be applied successfully to all combinations. Learning to choose an appropriate tool and apply it well is crucial.
Thank you for all contributions. They are very insightful. Allow me to flame a bit (don't take it personal, though :-)
Most people seem to think that formal methods are just about program verification. Or critical systems. This may be true if we pursue the ultimate cliche: to prove we are doing the program right (v.s. validation, which asks, as a contributor said, if we are doing the right program).
But consider model finding/checking tools, such as Alloy. Learning to use a tool like this takes a negligable ammount of time for anyone used to UML and OO. Still, it can give you immediate insight over your model. It usually takes no more than 10 minutes to find a counter-example over a small enough subset of the model one's trying to use (and that includes describing the model in Alloy in the first place).
Take requirements engineering as an example. One usually draw a lot of UML. Few people use OCL, though, and many business rules are informally annoted in natural language. Why? Time constraints?
Now consider the fact that the majority just uses her/his gut-feeling to prove that a model is satisfiable. Again, why? I can take the same amount of time (probably even less, since I don't need to care about drawing aesthetics) to write that model in Alloy, and just check for satisfiability? And what kind of mathematics do I need to now? "Predicates"? Fancy name for IFs and booleans ;-) Quantifiers? Fancy names for ForEachs()...
What about big information systems? They don't need to be critical... Just try to analyze in your head a conceptual (not implementation!) diagram with over 600 classes. I see many people banging their head in the wall with easy-to-make model mistakes because they missed some constraint, or the model allows stupid things to happen.
The fact is, one does not need to use formal approaches from head to tail. Granted, I could prove a whole application in Coq, and certify that it is 100% compliant with some specification. This may be the Computer Scientist/Mathematician approach.
Still, with a GTD philisophy, why can't I delegate some tasks for the computer and allow it to help improving my development? Is it really a matter of "time", or plain, simple lack of technical abilities and will to learn/inovate?
Working with line of business IT development in an enterprise means having to transfer knowledge about the business from actual business people into the heads of developers. While I myself find abstract maths to be one of the greatest pastimes there is, it's a terrible communications tool. And communications is what it's all about. While I might conceivably have some success convincing IT people to embrace more abstract notations, I basically have no chance with the business people.
While there are some areas where I can see a role for formal methods in an enterprise (math- and logic-heavy specialist software, significant need for provable properties as in safety critical software) they provide little help with getting correct requirements on e.g. how to fulfil a customer order by issuing one or more supply orders to a set of possible external or internal providers.
I think the jury is still out on model based approaches and domain specific languages. I think they will succeed or fail depending on whether they provide quicker feedback from IT to the wishes and needs of the business side, and whether they presume business people will have to do any significant studying.
Technology is easy. Communication is hard. Formal methods may help us do things right, but those I've seen do nothing to help us do the right things. (Yes, these are cliches, but that's because they're inescapably and painfully true.)
I'm taking a course on 'Specification and Verification'. As part of the course structure we are doing the following- 1. Learning tools like PVS(Prototype Verification System) http://pvs.csl.sri.com/ and SMV(Software Modeling and Verification) http://www.cs.cmu.edu/~modelcheck/smv.html 2. Apart from that we do dissect accidents which happened because of software failures. For e.g. - Failure of Ariane V
I feel formal methods are more applicable to scenarios where the failure cost is more than the design cost. And it seems apt to use them for softwares being used in critical systems. I guess it is used in avionics, chip design etc. and the current automobile industry is also drafting it into practice.
a.) 许多开发人员对正式方法所需的抽象级别感到不舒服。 大多数入门级数学教育都是微积分和非离散数学，这一事实可能与此有关。
b.) 正式方法需要一种非常自下而上的设计方法，从头开始设计核心模型并使其密不可分，然后通过在其之上提供接口将其连接到实际的用户需求。 由于我们倾向于让需求驱动开发工作，因此自上而下的方法感觉更自然，尽管它经常导致模型不一致。 这就像在你的房子建成后在下面改造一个地下室一样。
I have tried to get people to embrace formal specification methods a few times (Z and Alloy) and have made the same expirience that you have: Most people, while feeling that they serve a useful purpose, are very uncomfortable using them for actual work.
Funny enough, the same people are more than happy to produce utterly useless UML diagrams in ginormous quantities.
I think there are two main reasons for this:
a.) Many developers are uncomfortable with the level of abstraction required by a formal approach. The fact that most entry-level mathematics education is all calculus and non discrete-mathematics might have to do something with this.
b.) Formal methods require a very bottom up design aproach where you design your core model from the ground up and make it airtight and then connect it up to the actual user requirements by providing an interface on top of it. Since we tend to have requirements drive development efforts, a top-down approach feels more natural although it often leads to inconsistent models. It's like retrofitting a basement underneath your house after it has already been built.
在生产 Web 应用程序中，您有多个前端框、多个后端框、多个数据库框 - 如果其中任何一个上的程序失败，那不是事件。 硬件非常便宜，您构建这些系统的成本远远低于正式指定所有软件的成本。
Formal methods make no sense in systems where the cost of failure is low.
In a production web application, you've got multiple front-end boxes, multiple back-end boxes, multiple database boxes - if a program on any one of them fails, it's a non-event. Hardware is so cheap that you can build these systems for far less than the cost of formally specifying all your software.
发布评论
评论（6）
让人们接受任何方法或方法论的关键是向他们展示它如何解决他们遇到的问题。 如果他们能够看到这将使他们的生活变得更好，那么你就有更大的机会让他们采用这些技术。
如果您不能向他们展示这一点，也许您想采用基于哲学而不是实用性的方法。 除非其他人认同你的理念，否则你将一事无成。 也许你不应该。
几十年来，出现了很多方法论。 新的项目总是能解决旧项目的缺点，但项目仍然会遇到麻烦并失败。 为什么？ 因为提出新方法论的摇滚明星就是摇滚明星，并且正是因为他们了解根本问题以及如何应用它们而制定了新方法论。 后来的人往往会盲目照着食谱做，效果并不好。
所以我认为最好的办法是教授潜在的问题，然后展示各种方法如何尝试解决这些问题。 公司、项目和团队之间的差异如此之大，以至于没有一种方法可以成功地应用于所有组合。 学会选择合适的工具并很好地应用它至关重要。
The key to getting people to buy into any methods or methodologies is to show them how it solves problems they are having. If they can see it will make their lives better you have a much improved chance of getting them to adopt the techniques.
And if you can't show them that, perhaps you wanted to adopt the methods based on philosophy rather than practicality. Unless the others share your philosophy then you're not going to get anywhere. And perhaps you shouldn't.
Over the decades there have been a great many methodologies. Newer ones always address the shortcomings of the old ones, yet projects still get in trouble and fail. Why? Because the rock stars that come up with new methodologies are rock stars, and have made a new methodology precisely because they understand the underlying issues and how to apply them. Those who come after tend to blindly follow the recipe, and it doesn't work so well.
So I think the best thing is to teach about the underlying problems and then show how various methods attempt to deal with those problems. The differences in companies, projects, and teams is so great that no one methodology can be applied successfully to all combinations. Learning to choose an appropriate tool and apply it well is crucial.
感谢您的所有贡献。 他们非常有洞察力。 请允许我稍微发怒一下（不过，不要认为这是针对个人的:-)
大多数人似乎认为形式化方法只是关于程序验证。 或关键系统。 如果我们追求最终的陈词滥调：证明我们正在正确地执行程序（而不是验证，正如贡献者所说，验证询问我们是否正在执行正确的程序），这可能是正确的。
但请考虑模型查找/检查工具，例如 Alloy。 对于习惯 UML 和 OO 的人来说，学习使用这样的工具所花费的时间可以忽略不计。 尽管如此，它仍然可以让您立即了解您的模型。 通常需要不超过 10 分钟的时间就可以在尝试使用的模型的足够小的子集上找到反例（这包括首先在 Alloy 中描述模型）。
以需求工程为例。 一个人通常会画很多UML。 不过，很少有人使用 OCL，而且许多业务规则都是用自然语言非正式注释的。 为什么？ 时间限制？
现在考虑一下这样一个事实：大多数人只是用她/他的直觉来证明模型是可以令人满意的。 再说一遍，为什么？ 我可以花费相同的时间（可能甚至更少，因为我不需要关心绘图美学）在 Alloy 中编写该模型，然后检查是否可满足？ 我现在需要什么样的数学？ “谓词”？ IF 和布尔值的奇特名称;-) 量词？ ForEachs() 的奇特名称...
大信息系统怎么样？ 它们不需要很挑剔......只需尝试在头脑中分析包含 600 多个类的概念图（而不是实现！）。 我看到很多人因为容易犯的模型错误而碰壁，因为他们错过了一些约束，或者模型允许愚蠢的事情发生。
事实上，我们不需要从头到尾使用正式的方法。 当然，我可以在 Coq 中证明整个应用程序，并证明它 100% 符合某些规范。 这可能是计算机科学家/数学家的方法。
尽管如此，凭借 GTD 理念，为什么我不能向计算机委派一些任务并让它帮助改进我的开发呢？ 这真的是“时间”的问题，还是简单、简单的缺乏技术能力和学习/创新意愿的问题？
Thank you for all contributions. They are very insightful. Allow me to flame a bit (don't take it personal, though :-)
Most people seem to think that formal methods are just about program verification. Or critical systems. This may be true if we pursue the ultimate cliche: to prove we are doing the program right (v.s. validation, which asks, as a contributor said, if we are doing the right program).
But consider model finding/checking tools, such as Alloy. Learning to use a tool like this takes a negligable ammount of time for anyone used to UML and OO. Still, it can give you immediate insight over your model. It usually takes no more than 10 minutes to find a counter-example over a small enough subset of the model one's trying to use (and that includes describing the model in Alloy in the first place).
Take requirements engineering as an example. One usually draw a lot of UML. Few people use OCL, though, and many business rules are informally annoted in natural language. Why? Time constraints?
Now consider the fact that the majority just uses her/his gut-feeling to prove that a model is satisfiable. Again, why? I can take the same amount of time (probably even less, since I don't need to care about drawing aesthetics) to write that model in Alloy, and just check for satisfiability? And what kind of mathematics do I need to now? "Predicates"? Fancy name for IFs and booleans ;-) Quantifiers? Fancy names for ForEachs()...
What about big information systems? They don't need to be critical... Just try to analyze in your head a conceptual (not implementation!) diagram with over 600 classes. I see many people banging their head in the wall with easy-to-make model mistakes because they missed some constraint, or the model allows stupid things to happen.
The fact is, one does not need to use formal approaches from head to tail. Granted, I could prove a whole application in Coq, and certify that it is 100% compliant with some specification. This may be the Computer Scientist/Mathematician approach.
Still, with a GTD philisophy, why can't I delegate some tasks for the computer and allow it to help improving my development? Is it really a matter of "time", or plain, simple lack of technical abilities and will to learn/inovate?
在企业中进行业务线 IT 开发意味着必须将业务知识从实际业务人员转移到开发人员的头脑中。 虽然我自己发现抽象数学是最好的消遣之一，但它是一种糟糕的沟通工具。 沟通就是一切。 虽然我可能会成功地说服 IT 人员接受更抽象的符号，但我基本上没有机会与业务人员合作。
虽然在某些领域我可以看到形式化方法在企业中的作用（数学和逻辑密集的专业软件，对可证明属性的巨大需求，如安全关键软件），但它们对于获得正确的要求（例如如何通过向一组可能的外部或内部供应商发出一个或多个供应订单来履行客户订单。
我认为对于基于模型的方法和特定于领域的语言还没有定论。 我认为他们的成功或失败取决于他们是否能更快地从 IT 处提供反馈来满足业务方面的愿望和需求，以及他们是否认为业务人员必须进行任何重要的学习。
技术很容易。 沟通很困难。 正式的方法可能会帮助我们做正确的事情，但我所见过的那些方法并不能帮助我们做正确的事情。 （是的，这些都是陈词滥调，但那是因为它们是不可避免的、令人痛苦的事实。）
Working with line of business IT development in an enterprise means having to transfer knowledge about the business from actual business people into the heads of developers. While I myself find abstract maths to be one of the greatest pastimes there is, it's a terrible communications tool. And communications is what it's all about. While I might conceivably have some success convincing IT people to embrace more abstract notations, I basically have no chance with the business people.
While there are some areas where I can see a role for formal methods in an enterprise (math- and logic-heavy specialist software, significant need for provable properties as in safety critical software) they provide little help with getting correct requirements on e.g. how to fulfil a customer order by issuing one or more supply orders to a set of possible external or internal providers.
I think the jury is still out on model based approaches and domain specific languages. I think they will succeed or fail depending on whether they provide quicker feedback from IT to the wishes and needs of the business side, and whether they presume business people will have to do any significant studying.
Technology is easy. Communication is hard. Formal methods may help us do things right, but those I've seen do nothing to help us do the right things. (Yes, these are cliches, but that's because they're inescapably and painfully true.)
我正在学习“规范和验证”课程。 作为课程结构的一部分，我们正在做以下事情：
1. 学习工具如PVS（原型验证系统）http://pvs.csl.sri.com/ 和 SMV（软件建模和验证）http://www.cs.cmu .edu/~modelcheck/smv.html
2. 除此之外，我们还会剖析因软件故障而发生的事故。 例如，Ariane V 的故障
我认为形式化方法更适用于故障成本大于设计成本的情况。 而且似乎很容易将它们用于关键系统中使用的软件。 我猜它用在航空电子设备、芯片设计等方面，目前汽车行业也正在将其付诸实践。
I'm taking a course on 'Specification and Verification'. As part of the course structure we are doing the following-
1. Learning tools like PVS(Prototype Verification System) http://pvs.csl.sri.com/ and SMV(Software Modeling and Verification) http://www.cs.cmu.edu/~modelcheck/smv.html
2. Apart from that we do dissect accidents which happened because of software failures. For e.g. - Failure of Ariane V
I feel formal methods are more applicable to scenarios where the failure cost is more than the design cost. And it seems apt to use them for softwares being used in critical systems. I guess it is used in avionics, chip design etc. and the current automobile industry is also drafting it into practice.
我曾多次尝试让人们接受形式化规范方法（Z 和 Alloy），并获得了与您相同的经验：大多数人虽然感觉它们具有有用的用途，但在实际工作中使用它们却感到非常不舒服。
有趣的是，同样的人非常乐意大量生成完全无用的 UML 图。
我认为这有两个主要原因：
a.) 许多开发人员对正式方法所需的抽象级别感到不舒服。 大多数入门级数学教育都是微积分和非离散数学，这一事实可能与此有关。
b.) 正式方法需要一种非常自下而上的设计方法，从头开始设计核心模型并使其密不可分，然后通过在其之上提供接口将其连接到实际的用户需求。 由于我们倾向于让需求驱动开发工作，因此自上而下的方法感觉更自然，尽管它经常导致模型不一致。 这就像在你的房子建成后在下面改造一个地下室一样。
I have tried to get people to embrace formal specification methods a few times (Z and Alloy) and have made the same expirience that you have: Most people, while feeling that they serve a useful purpose, are very uncomfortable using them for actual work.
Funny enough, the same people are more than happy to produce utterly useless UML diagrams in ginormous quantities.
I think there are two main reasons for this:
a.) Many developers are uncomfortable with the level of abstraction required by a formal approach. The fact that most entry-level mathematics education is all calculus and non discrete-mathematics might have to do something with this.
b.) Formal methods require a very bottom up design aproach where you design your core model from the ground up and make it airtight and then connect it up to the actual user requirements by providing an interface on top of it. Since we tend to have requirements drive development efforts, a top-down approach feels more natural although it often leads to inconsistent models. It's like retrofitting a basement underneath your house after it has already been built.
在失败成本较低的系统中，形式化方法没有任何意义。
在生产 Web 应用程序中，您有多个前端框、多个后端框、多个数据库框 - 如果其中任何一个上的程序失败，那不是事件。 硬件非常便宜，您构建这些系统的成本远远低于正式指定所有软件的成本。
Formal methods make no sense in systems where the cost of failure is low.
In a production web application, you've got multiple front-end boxes, multiple back-end boxes, multiple database boxes - if a program on any one of them fails, it's a non-event. Hardware is so cheap that you can build these systems for far less than the cost of formally specifying all your software.