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.

People involved:

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.