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 Small.thy

Sprache: Isabelle

section ‹Smaller End of Deque›

theory Small
imports Common
begin

text ‹
🪙 The smaller end of the deque during ‹Rebalancing› can be in one three phases:

🪙 ‹Small1›: Using the ‹step› function the originally contained elements are reversed.
🪙 ‹Small2›: Using the ‹step› function the newly obtained elements from the bigger end are reversed on top of the ones reversed in the previous phase.
🪙 ‹Small3›: See theory ‹Common›. Is used to reverse the elements from the two previous phases again to get them again in the original order.

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

datatype (plugins del: size) 'a small_state =
   Small1 "'a current" "'a stack" "'a list"
| Small2 "'a current" "'a list" "'a stack" "'a list" nat
| Small3 "'a common_state"

text ‹🪙 Functions:

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

instantiation small_state::(type) step
begin

fun step_small_state :: "'a small_state ==> 'a small_state" where
  "step (Small3 state) = Small3 (step state)"
| "step (Small1 current small auxS) = (
    if is_empty small
    then Small1 current small auxS
    else Small1 current (Stack.pop small) ((Stack.first small)#auxS)
  )"
| "step (Small2 current auxS big newS count) = (
    if is_empty big
    then Small3 (normalize (Copy current auxS newS count))
    else Small2 current auxS (Stack.pop big) ((Stack.first big)#newS) (count + 1)
  )"

instance..
end

fun push :: "'a ==> 'a small_state ==> 'a small_state" where
  "push x (Small3 state) = Small3 (Common.push x state)"
| "push x (Small1 current small auxS) = Small1 (Current.push x current) small auxS"
| "push x (Small2 current auxS big newS count) =
    Small2 (Current.push x current) auxS big newS count"

fun pop :: "'a small_state ==> 'a * 'a small_state" where
  "pop (Small3 state) = (
    let (x, state) = Common.pop state
    in (x, Small3 state)
  )"
| "pop (Small1 current small auxS) =
    (first current, Small1 (drop_first current) small auxS)"
| "pop (Small2 current auxS big newS count) =
    (first current, Small2 (drop_first current) auxS big newS count)"

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.11 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.