Note 17 Mike Lowry
SW productivity in SW has only improved 1 O magnitude
Question: but SW is no often 10^6 times as big?
Software is the only thing that you can change after delivery, especially on a spacecraft.
89% of cost is maintenance, 50% of that is needed for understanding.
Same origin of research as Mike DeBellis: Balzer, Green, Luckham, Rich, et al.
KBSE(A) and Formal SW Methods have not had much impact.
Program synthesis (KIDS) requires sophisticated users.
Knowledge-based code generation did not inspire confidence (viz Stanford Radio Astronomy)
Declarative sematics are easier to follow than operational semantics, as
are commonly used in AI systems.
Difficult to get forma specification of problems.
Amphion (defended Thebes by making wall through Lyre music)
1. provides a Scruffy GUI that is easier, (Gerhard Fisher's)
2. (Generic) theorrm prover which takes a domain theory
defined by specialist
Next: Meta-Amphion (shell) to develop generic tools for domain theory creation.
1. End users
2. Domain experts
3. Formal method (AI) expert
Experience with Amphion NAIF (navigation), other Amphions for shuttle, for xxxx
NAIF libray is 600+ Fortran 77 library, well-documented, but requires a user investment to use, i.e., reuse.
Solution: graphical program description.
300 axioms, 60% routine coverage.
Meta-Amphion is to generate domain theories
Specware has an algebra over domains. based on colimits and categories.