Formal methods in game development.
Author
First of all, I don't know anything about the subject, so if I use terminology incorrectly, or sound completely incoherent, then I do apologise. [smile]
But I'm curious. Does anyone here ever make use of any formal methods before writing an engine, or indeed any other software for a game? Given that such techniques are rarely used (effectively) in industrial software in general, I don't suppose it's common in the gaming industry. But at the same time, surely it should be?
It seems that most of the companies that successfully use formal methods can deliver much more reliable software at significantly lower costs than their competition. There's a bit on Praxis High Integrity Systems' website I particularly like: they've developed software that's significantly more reliable than that used by the Space Shuttle, and at a fifth of the industry standard cost. (Incidentally, I've recently been ranted to at length by Praxis founder Martyn Thomas in a short series of lectures. An interesting point he made was that, IIRC, there are more development houses in India which can successfully utilize formal methods than in the rest of the world combined. Why are other countries so far behind?)
Now, clearly a game doesn't need to achieve industrial grade reliability. Indeed, with the languages and technologies commonly used, that's probably impossible. But surely there's a lot of room for improvement? A program that's the result of careful analysis and design is guaranteed to be much more reliable, and will be cheaper to build, than results obtained by other methods.
So why don't people do this?
This is where I'm totally ignorant. Is it because such techniques aren't fully understood within the industry? Is it because of a lack of will to adopt new methods? Is it because the current languages of choice are particularly difficult to reason about? Or is it simply not worth applying these techaniques to something as "trivial" as a game engine? If it's the latter case, then why are games so notoriously buggy? If it's not, then why aren't formal methods used more frequently? Or are such techniques only useful when applied to larger systems, and, if so, will game engines become large enough to warrant such methods in the near future?
EDIT: Some spelling.
Warning: a lot of what I am about to say is not generally agreed upon, but is merely my observations from 17 years of personal, academic, and commercial development.
I have never seen any convincing evidence to suggest that is the case, except where it was evidence based on another industry (eg. engineering).
The theory goes that formal methods help turn poor and mediocre developers into reasonable ones. They don't help turn good developers into great ones. Perhaps in India there are lots of mediocre developers who companies are interested in making use of. (No offense to any non-mediocre developers from India who are reading.)
Personally I think 'software engineering' is a great mistake. It mistakes the source code for the product when generally the source code is just the design for the product. It emphasises rigidity and process over creativity and ingenuity, another mistake when given the expressiveness of high level programming languages and intelligent users. It also ignores the differences inherent to software that make development so different to other forms of engineering, such as the ability to prototype ideas virtually for free.
Well, it's not guaranteed at all. Let's not mistake a few people trying to promote their company or book with proven facts. There is very little proven when it comes to software development.
One major problem: game software very rarely has a specification to meet. When Praxis have to develop a program, they almost certainly have a client who has very strict requirements that need meeting. Thus, specifications can be drawn up and analysis and design can be done with that in mind. You cannot do this with 99% of games, for at least 2 reasons - firstly, there is no specific customer who is specifying what is needed, and secondly, games are rooted in human psychology, pop culture, and rapidly changing market forces, making accurate and detailed specification not only difficult but probably pointless.
Formal methods tend to be like an inverted pyramid, balancing implementation precariously on top of design, itself balancing on top of analysis, which sits above the specification. Not only does the absence of a clear specification make it incredibly difficult to produce a clear analysis/design/implementation, but by definition it makes it almost impossible to judge the success of those stages as there isn't a fixed set of exacting criteria to meet. I think the success of formal methods always requires measurement against a known target.
More recently 'extreme programming' is coming forward as a new method of interest, but I doubt it would be taken seriously by those who espouse the type of formalism you are talking about.
This is another problem, although by far not the main reason. It's quite easy to write robust software in ADA as the language was designed from the beginning to be robust. On the other hand, C++ was designed to provide high level facilities on top of low-level power, and as such is almost the opposite.
You can ask why games are buggy, but you could also ask why Praxis's software is not fun. Given limited resources, any company will address the key needs first. I don't think there's much excuse for the poor reliability of most game programs, but the fact is that the software is not mission critical, and has a very short execution life. Given X dollars/hours to spend on the software, both customer satisfaction and revenue for a game program will be maximised by adding gameplay and features over fixing a bug here and there.
Quote:Original post by MumbleFuzz
It seems that most of the companies that successfully use formal methods can deliver much more reliable software at significantly lower costs than their competition.
I have never seen any convincing evidence to suggest that is the case, except where it was evidence based on another industry (eg. engineering).
Quote:(Incidentally, I've recently been ranted to at length by Praxis founder Martyn Thomas in a short series of lectures. An interesting point he made was that, IIRC, there are more development houses in India which can successfully utilize formal methods than in the rest of the world combined. Why are other countries so far behind?)
The theory goes that formal methods help turn poor and mediocre developers into reasonable ones. They don't help turn good developers into great ones. Perhaps in India there are lots of mediocre developers who companies are interested in making use of. (No offense to any non-mediocre developers from India who are reading.)
Personally I think 'software engineering' is a great mistake. It mistakes the source code for the product when generally the source code is just the design for the product. It emphasises rigidity and process over creativity and ingenuity, another mistake when given the expressiveness of high level programming languages and intelligent users. It also ignores the differences inherent to software that make development so different to other forms of engineering, such as the ability to prototype ideas virtually for free.
Quote:A program that's the result of careful analysis and design is guaranteed to be much more reliable, and will be cheaper to build, than results obtained by other methods.
So why don't people do this?
Well, it's not guaranteed at all. Let's not mistake a few people trying to promote their company or book with proven facts. There is very little proven when it comes to software development.
One major problem: game software very rarely has a specification to meet. When Praxis have to develop a program, they almost certainly have a client who has very strict requirements that need meeting. Thus, specifications can be drawn up and analysis and design can be done with that in mind. You cannot do this with 99% of games, for at least 2 reasons - firstly, there is no specific customer who is specifying what is needed, and secondly, games are rooted in human psychology, pop culture, and rapidly changing market forces, making accurate and detailed specification not only difficult but probably pointless.
Formal methods tend to be like an inverted pyramid, balancing implementation precariously on top of design, itself balancing on top of analysis, which sits above the specification. Not only does the absence of a clear specification make it incredibly difficult to produce a clear analysis/design/implementation, but by definition it makes it almost impossible to judge the success of those stages as there isn't a fixed set of exacting criteria to meet. I think the success of formal methods always requires measurement against a known target.
More recently 'extreme programming' is coming forward as a new method of interest, but I doubt it would be taken seriously by those who espouse the type of formalism you are talking about.
Quote:Is it because the current languages of choice are particularly difficult to reason about?
This is another problem, although by far not the main reason. It's quite easy to write robust software in ADA as the language was designed from the beginning to be robust. On the other hand, C++ was designed to provide high level facilities on top of low-level power, and as such is almost the opposite.
Quote:...why are games so notoriously buggy? If it's not, then why aren't formal methods used more frequently?
You can ask why games are buggy, but you could also ask why Praxis's software is not fun. Given limited resources, any company will address the key needs first. I don't think there's much excuse for the poor reliability of most game programs, but the fact is that the software is not mission critical, and has a very short execution life. Given X dollars/hours to spend on the software, both customer satisfaction and revenue for a game program will be maximised by adding gameplay and features over fixing a bug here and there.
Formal methods of specification is particularly useful in the analysis & design of safety critical systems such as software for hospitals obviously because somebody's life is at the stake of a piece of software.
Formals methods uses mathematics & mathematical notation to unambiguously specify a system, meaning when people look at the specification it means the same thing to everyone (who can read it) unlike the english language which is informal & ambiguous, a sentance can mean slightly different things to different people. UML is considered semi-formal.
Formals methods are not new they've been around for a while. When i was at uni i was taught Z my formals methods teacher told me in the UK, Z is dominantly taught while in US VDM is more taught.
In the context of games development i highly doubt a single development team use any form of formal methods or even know they exist.
If they do know about them they probably wont use it for fact of the matter:
Formal spec language has a high learning curve, you need to be quite mathematically & logically minded, this might be unproductive to get new employees to learn.
Writing a formal specification takes time, you'll spend ages just on requirements & analysis, you'll initially end up with a requirements specification written in mathematics does that sound appealing to you? [grin].
If i remeber correctly relizing a formal specification into a programming language requires repeated refinement as the initial spec is to high level, this takes time.
[Edited by - snk_kid on June 17, 2005 4:13:17 AM]
Formals methods uses mathematics & mathematical notation to unambiguously specify a system, meaning when people look at the specification it means the same thing to everyone (who can read it) unlike the english language which is informal & ambiguous, a sentance can mean slightly different things to different people. UML is considered semi-formal.
Formals methods are not new they've been around for a while. When i was at uni i was taught Z my formals methods teacher told me in the UK, Z is dominantly taught while in US VDM is more taught.
In the context of games development i highly doubt a single development team use any form of formal methods or even know they exist.
If they do know about them they probably wont use it for fact of the matter:
Formal spec language has a high learning curve, you need to be quite mathematically & logically minded, this might be unproductive to get new employees to learn.
Writing a formal specification takes time, you'll spend ages just on requirements & analysis, you'll initially end up with a requirements specification written in mathematics does that sound appealing to you? [grin].
If i remeber correctly relizing a formal specification into a programming language requires repeated refinement as the initial spec is to high level, this takes time.
[Edited by - snk_kid on June 17, 2005 4:13:17 AM]
Author
Thanks for the replies, guys. Very enlightening.
Looking back at my original post, I think I should have elaborated a little. I realised pretty much while I was writing it that, in the game industry, there's no real need for a completely formal approach. But are there ways in which some of the ideas can be usefully applied?
After all, one of the reasons OOP programming is so useful is that it allows you to form the program at a more abstract level. Is it not possible, for example, to reason about object interaction in a more formal way?
True, but it's also very well documented how unsuccessful current design techniques are on complex systems. In any case, Thomas wasn't trying to promote his company, he was trying to promote what he believed were essential changes that needed to be made in the software industry. I've never heard anyone talk so passionately about their subject, which is part of the reason I'm intrigued by the ideas he mentioned.
In any case, it's something I hope to learn more about, if only for academic purposes.
Looking back at my original post, I think I should have elaborated a little. I realised pretty much while I was writing it that, in the game industry, there's no real need for a completely formal approach. But are there ways in which some of the ideas can be usefully applied?
After all, one of the reasons OOP programming is so useful is that it allows you to form the program at a more abstract level. Is it not possible, for example, to reason about object interaction in a more formal way?
Quote:Well, it's not guaranteed at all. Let's not mistake a few people trying to promote their company or book with proven facts. There is very little proven when it comes to software development.
True, but it's also very well documented how unsuccessful current design techniques are on complex systems. In any case, Thomas wasn't trying to promote his company, he was trying to promote what he believed were essential changes that needed to be made in the software industry. I've never heard anyone talk so passionately about their subject, which is part of the reason I'm intrigued by the ideas he mentioned.
Quote:Formals methods are not new they've been around for a while.I know. Didn't Turing suggest such methods as long ago as 1950 or so?
In any case, it's something I hope to learn more about, if only for academic purposes.
Quote:Original post by MumbleFuzz
After all, one of the reasons OOP programming is so useful is that it allows you to form the program at a more abstract level. Is it not possible, for example, to reason about object interaction in a more formal way?
One of the benifits of game development is often that object interactions are far more understandable as the objects are based very solidly on actual objects.
For instance, a "DatabaseTransaction" object is fairly abstract. Whereas the objects you deal with in game development are not very far removed from reality. A game might have a "Weapon" object or an "Enemy" object - it's pretty clear already what each object does, how it interacts, etc. (Additionally, this is one of the reasons OOP is idealy suited to game development.)
Thus, rather than waste time formalising already-obvious interactions, game developers can leap straight into code. Also, as Kylotan said before, changing the software and prototyping is virtually zero-cost when avoiding most formal methods. If a mistake is made, it's fairly easy just to go in and correct it in the source itself.
In other words, the game developer can say "Right, we probably need a weapon object that shoots enemy objects - now go forth and program it", whereas the programmer on the formal system has to go "Right, we are going to have DatabaseTransaction object, it is used by X for Y and Z for Q, it has methods A, B and C, and lifetime L, it is responsible for R, S and T, etc, etc, etc, etc, etc".
Also, game developers can take advantage of small and often local development teams. So any design problems that come up when basically designing-in-source can be sorted out quickly.
Formal specifications are not a really good solution in the field of game programming.
They can be used to design the more concretely specified components, such as any mathematical components you have but, as has been pointed out, they can't design as component whose specification is more fuzzy.
For example, how would you specificy a particle effect that looks like an explosion? You could formally specify the maximum number of particles, how they're updated with respect to time etc. but you can't specify the most important thing - that the effect looks good.
In a similar note you can't specify a RNG in a formal language as the specification is simply that it appears to produce a series of random numbers.
They can be used to design the more concretely specified components, such as any mathematical components you have but, as has been pointed out, they can't design as component whose specification is more fuzzy.
For example, how would you specificy a particle effect that looks like an explosion? You could formally specify the maximum number of particles, how they're updated with respect to time etc. but you can't specify the most important thing - that the effect looks good.
In a similar note you can't specify a RNG in a formal language as the specification is simply that it appears to produce a series of random numbers.
Quote:Original post by MumbleFuzz
After all, one of the reasons OOP programming is so useful is that it allows you to form the program at a more abstract level. Is it not possible, for example, to reason about object interaction in a more formal way?
I think so, for example in UML you have the object constraint language (OCL)
Quote:
The Object Constraint Language - the OCL is used to specify constraints on objects in the UML. It has the power (but not syntax) of the Lower order Predicate Calculus (LPC) plus simple set_theory.
OCL isn't used on its own its not mean't to fully specifiy a system, its used in conjunction with UML diagrams.
Quote:Original post by MumbleFuzz
In any case, it's something I hope to learn more about, if only for academic purposes.
If you like/liked discrete maths then you will probably like taking a module on a formal methods, i found it interesting even if it isn't particularly useful for games developement.
[Edited by - snk_kid on June 17, 2005 10:11:31 AM]
Quote:Original post by MumbleFuzz
Looking back at my original post, I think I should have elaborated a little. I realised pretty much while I was writing it that, in the game industry, there's no real need for a completely formal approach. But are there ways in which some of the ideas can be usefully applied?
After all, one of the reasons OOP programming is so useful is that it allows you to form the program at a more abstract level. Is it not possible, for example, to reason about object interaction in a more formal way?
Mainly I was complaining about the problem of relying too heavily on specifications in game development, which are rarely present or complete and therefore inhibits the use of formal methodologies (eg. waterfall model) or mathematical constraints (eg. specifications in Z) on the system as a whole. I suppose you can use the formal methods on individual components, but again you have the overhead of laying down a precise specification, agreeing the logic that applies to it all, then verifying it, all in the face of change, disagreements over logic, requests for flexibility and 'forward compatibility', etc. And the more rigidly you specify an object, the more assumptions are made about it by other objects, and then when change does happen, it ripples through your ossified project, breaking everything as it goes along. I am very wary of anything that attempts to lock specifications in stone as I consider this (a) impractical, and (b) too closely modelling software development on totally different disciplines (ie. ones that do actually need big up-front design).
I believe a better approach for the same sort of situation is test-based development. Basically you develop your software component hand in hand with tests that verify that it works according to plan. It's much less formal and accordingly things could fall through the cracks, but it's more practical, more intuitive, requires less additional learning on the part of the developer, and is more easily automated than formal constraint checking.
Quote:True, but it's also very well documented how unsuccessful current design techniques are on complex systems.
Unfortunately, that isn't a logical argument for using formal methods. Absence of something + failure doesn't imply presence of something comes with success. I have failed to complete many projects without wearing a chicken on my head while I was coding; should I try the poultry hat next time? ;)
Quote:Original post by Kylotan
I have failed to complete many projects without wearing a chicken on my head while I was coding; should I try the poultry hat next time? ;)
Yes! And I suggest you photographicly document it and post it here so others may benifit from your experience [lol].
Lets hope that formal methods never become popular is game development. Game development would become a whole lot less fun, alot more academic and games will be even less original than they are now!
This topic is closed to new replies.
Advertisement
Popular Topics
Advertisement
