Technology : The impossible art of killing bugs…

时间:2019-02-27 12:19:04166网络整理admin

By David Brake AS Benjamin Franklin might have said, you can be sure of three things in life: death, taxes and bugs in software. British software company IMS can’t do much about the first two but it is hoping to reduce the third with Escher—an application which it claims produces error-free programs. Software developers usually break down what they are trying to do into functions. Routines are written for functions and bolted together to make a whole program. Conflicts between functions or mistakes during coding can cause bugs. In contrast, Escher helps software writers describe what they are trying to do in abstract, logical terms. These logical arguments can be mathematically proven to be free of errors. Armed with this description Escher will generate the software itself or—if the program is complex—check the programmer has done what they intended. Formal specification languages like Z and Larch that use formal logic have been around for nearly 30 years but are difficult to use because they demand a thorough grounding in mathematics says David Crocker, chairman and technical director of IMS. Escher does use a formal specification language but it will never be seen. Instead programmers will build up software using short programs called objects. Different objects will represent logical expressions. “It still contains first order predicate calculus, but in a friendly way—you won’t hear it called that in the manual,” says Crocker. IMS has been developing Escher for 18 months and will have a first version ready late next year. Initially it will only be able to write new programs. Later IMS wants to make a version that can analyse existing software and pick out errors. To avoid bugs in the Escher software, it has been used to check itself during development. However, Tom Anderson, director of the Centre for Software Reliability at the University of Newcastle upon Tyne, warns that not all software bugs are down to faulty logic. “Most studies indicate the majority of errors arise in the early stages when you are trying to define your goals,