Beweren en bewijzen/de zuilen/Formalisering/8. Parametrisatie

literatuur ...

De algemene vorm van de correctheidsstelling voor systemen

∀ φ, ∀ ψ, ∀ Φ, ∀ Ψ,
        Π(φ, ψ, Φ, Ψ)
    →
            N ∧ (∀ i ∈ {1, 2, ..., n}, ai(φi) → ci(ψi))
        →
            A(Φ) → C(Ψ)

Hierbij betekent:

• a_i(φ_i) → c_i(ψ_i) is de specificatie van onderdeel i.
• A(Φ) → C(Ψ) is de specificatie van het geheel.
• φ en ψ zijn de parameters van de onderdelen en Φ en Ψ de parameters van het geheel. Met deze parameters kun je een specificatie algemener maken, zodat ze b.v. geldt voor snelle en langzame onderdelen.
• Π(φ, ψ, Φ, Ψ) geven algemene voorwaarden aan zodat de parameters bij elkaar passen.
• N geeft relevante natuurwetten en domeinkennis aan.