Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Real_Time_Deque/ (Sammlung formaler Beweise Version 2026-5^©) Datei vom 29.4.2026 mit Größe 2 kB

Quelle Common.thy

Sprache: Isabelle

section ‹Common›

theory Common
imports Current Idle
begin

text ‹
🪙 The last two phases of both deque ends during rebalancing:

🪙 ‹Copy›: Using the ‹step› function the new elements of this deque end are brought back into the original order.
🪙 ‹Idle›: The rebalancing of the deque end is finished.

🪙 Each phase contains a ‹current› state, that holds the original elements of the deque end.
›

datatype (plugins del: size)'a common_state =
      Copy "'a current" "'a list" "'a list" nat
    | Idle "'a current" "'a idle"

text‹
🪙 Functions:

🪙 ‹push›, ‹pop›: Add and remove elements using the ‹current› state.
🪙 ‹step›: Executes one step of the rebalancing, while keeping the invariant.›

(* TODO: Maybe inline function? *)
fun normalize :: "'a common_state ==> 'a common_state" where
  "normalize (Copy current old new moved) = (
    case current of Current extra added _ remained ==>
      if moved ≥ remained
      then Idle current (idle.Idle (Stack extra new) (added + moved))
      else Copy current old new moved
  )"

instantiation common_state ::(type) step
begin

fun step_common_state :: "'a common_state ==> 'a common_state" where
  "step (Idle current idle) = Idle current idle"
| "step (Copy current aux new moved) = (
    case current of Current _ _ _ remained ==>
      normalize (
        if moved < remained
        then Copy current (tl aux) ((hd aux)#new) (moved + 1)
        else Copy current aux new moved
      )
  )"

instance..
end

fun push :: "'a ==> 'a common_state ==> 'a common_state" where
  "push x (Idle current (idle.Idle stack stackSize)) =
      Idle (Current.push x current) (idle.Idle (Stack.push x stack) (Suc stackSize))"
| "push x (Copy current aux new moved) = Copy (Current.push x current) aux new moved"

fun pop :: "'a common_state ==> 'a * 'a common_state" where
  "pop (Idle current idle) = (let (x, idle) = Idle.pop idle in (x, Idle (drop_first current) idle))"
| "pop (Copy current aux new moved) =
      (first current, normalize (Copy (drop_first current) aux new moved))"

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.