pith. sign in

arxiv: 2605.15001 · v1 · pith:SFOV44UHnew · submitted 2026-05-14 · 💻 cs.LO

Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements

Enguerrand Prebet , Andr\'e Platzer This is my paper

Pith reviewed 2026-06-30 19:28 UTC · model grok-4.3

classification 💻 cs.LO
keywords hybrid systemsrefactoringdifferential refinement logicproved refinementscyber-physical systemssafety preservationmodular verification
0
0 comments X

The pith

Hybrid system refactorings preserve required properties when expressed as propositions in differential refinement logic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proposes representing refactorings of hybrid systems as propositions within differential refinement logic. This allows proving that a refactored system maintains the original properties by transferring the proof along the modification. A sympathetic reader would care because iterative design of cyber-physical systems otherwise requires full safety rechecks after every change. The method handles multiple refactoring types, including those that add auxiliary variables, and supports either automatic proofs or proofs that stay modular and local to the change.

Core claim

Refactorings are represented as propositions in dRL, with a method for proving that system refactorings preserve their required properties by transferring the proof along the respective modification; these can be proved automatically or reduce to a modular proof solely about the local change.

What carries the argument

The refactoring-as-propositions principle, which uses refinements in differential refinement logic to simultaneously express system properties and the relation between an original hybrid system and its refactored version.

If this is right

  • Changes to a hybrid system can be checked for property preservation without re-verifying the entire system.
  • Proofs of required properties transfer directly from the original system to the refactored one.
  • Refactorings that introduce auxiliary variables are covered by the same uniform treatment as other changes.
  • Verification effort reduces to either fully automatic checks or modular proofs focused only on the local modification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Iterative design loops for cyber-physical systems could become faster while retaining formal safety guarantees.
  • Similar proposition-based transfer techniques might apply to refactorings in other formalisms or system classes.
  • Verification tools could be extended to automate the proof-transfer step for common local changes.
  • The approach emphasizes modularity, which could reduce the cost of maintaining large verified models over time.

Load-bearing premise

Differential refinement logic supplies a uniform way to express different hybrid-system refactorings while referring both to system properties and to the relation between original and changed versions.

What would settle it

A concrete hybrid-system refactoring known to preserve safety that cannot be proved to do so inside differential refinement logic, or a refactoring that alters safety yet receives an incorrect preservation proof.

Figures

Figures reproduced from arXiv: 2605.15001 by Andr\'e Platzer, Enguerrand Prebet.

Figure 1
Figure 1. Figure 1: Some dRL axioms and rules reasoning to reduce the expression in blue by a simpler one, where the hybrid programs are decomposed in simpler subprograms. KeYmaera X. The theorem prover KeYmaera X [11] implements dL, and more recently its microkernel now also supports its extension dRL [23]. It uses a uni￾form substitution calculus version[20,23] of the one presented here. Axioms are expressed directly in the… view at source ↗
Figure 2
Figure 2. Figure 2: Refactor template for box in context via global refinement Its soundness revolves around the notion of monotone (resp. antitone) con￾texts. Contexts are expressions (formulas or programs) with a hole. The hole ·p (resp. ·f ) expects a program (resp. a formula), and we denote by C(e) the ex￾pression obtained by substituting the hole by the expression e assuming the kind are respected. Monotone (resp. antito… view at source ↗
Figure 3
Figure 3. Figure 3: Refactor template via global program equivalence Having both these templates transforms simple dRL axioms into refactoring techniques, allowing to freely rewrite hybrid programs during the proofs. For instance, with dist-l, dist-r, ODE, and ∪l , we immediately obtain formal generic [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Program refactorings induced by global refinements 3.2 Local Refinement Sometimes, local changes are only justified due to the surrounding context. For instance, a test may evaluate to false due to a previous assignment, making one side of a choice α ∪ γ unreachable. In that case, the other direction for the refactorings (R9–10) of [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Refactor template via local refinement Program Equivalence. In order to preserve local information, program equiva￾lences need to be treated in the same way as local refinements. As the projective context Cα is dependent on the structure of C, the congruence cannot be imple￾mented in just one rule like with Section 3.1. Corollary 1. For a program context C, the following rule is derivable in dRL: Γ ⊢ Cα(α … view at source ↗
Figure 6
Figure 6. Figure 6: Refactor template via ghost refinement Handling loops. Looking at the induction case for loops, we want to automat￾ically derive (C(α); x := ∗) ∗ ; x := ∗ = C(α) ∗ ; x := ∗. Due to the repetition, even though the assignment is after the program, it may influence the execu￾tion before the next iteration. Thus, the proof of the equivalence above relies on (x := ∗; C(α); x := ∗) = C(α); x := ∗, which only hol… view at source ↗
Figure 7
Figure 7. Figure 7: Event and time-triggered systems time t and may only stop at the latest every T seconds. Thus, for this model to be still correct, it should react preemptively, so the condition for accelerating should be stronger, and depends on T. This is expressed in the hybrid program time from [PITH_FULL_IMAGE:figures/full_fig_p014_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Event-triggered to time-triggered system full system is automatic. Refactoring (R4) is similar but updates the domain constraint. Since the change occurs inside a differential equation, the resulting lemma is more complex. Indeed, we must show that [plant, t′ = 1 & t ≤ T]x ≤ θ holds locally, i.e., after running the updated controller. This is the essence of the transformation from event-triggered to time-t… view at source ↗
Figure 9
Figure 9. Figure 9: Axiom as rule with the corresponding proof The derivation is done by induction on the context C ± k1,k2 . The inference does not depend on the type of hole (k2), only the constructors and the polarities, thus the inference used generic names – αi , βi for programs, ϕi , ψi for formulas – to increase readability. The case for first-order logic constructs are standard and are omitted. In line with the implem… view at source ↗
read the original abstract

Cyber-physical systems are inherently complex due to their connection between software and the physical world. Iterative design reduces their complexity, but increases the need to repeatedly recheck their safety in full after every change. We introduce the refactoring-as-propositions principle in which refactorings are represented as propositions along with a method for proving that system refactorings preserve their required properties by transferring the proof along the respective modification. It is based on differential refinement logic (dRL), with which one can simultaneously and rigorously refer to properties of the systems and the relation between a refactored system and its original version. Refinements represent a uniform way of expressing different types of hybrid system refactorings, including those that introduce auxiliary variables. Furthermore, we show how these refactorings can be proved automatically, and/or reduce to a modular proof solely about the local change rather than about the whole system.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The paper introduces the refactoring-as-propositions principle for hybrid systems. Refactorings are represented as propositions in differential refinement logic (dRL), enabling proofs that system properties are preserved under refactoring by transferring proofs along the modification. dRL is claimed to provide a uniform representation for multiple refactoring types (including auxiliary-variable introductions) while allowing simultaneous reference to system properties and the original/refactored relation; the resulting proofs are said to be automatable or reducible to modular local arguments about the change alone.

Significance. If the uniformity claim and the proof-transfer mechanism are substantiated with concrete definitions and derivations, the work would offer a practical formal method for safe iterative refactoring of cyber-physical systems without full re-verification. This directly addresses a recurring pain point in hybrid-system design and would constitute a meaningful extension of dRL if the added principles are shown to be independent of prior results.

major comments (2)
  1. The abstract asserts that dRL supplies a uniform representation for refactorings (including auxiliary-variable cases) while simultaneously referring to properties and the original/refactored relation, yet no definitions of the relevant dRL propositions, refinement relations, or proof rules appear in the supplied material. Without these, the central uniformity and proof-transfer claims cannot be verified and remain load-bearing for the entire contribution.
  2. No concrete example, derivation, or proof sketch is supplied to illustrate how a refactoring proposition is formed, how proof transfer occurs, or how automation or modularity is achieved. This absence prevents assessment of whether the refactoring-as-propositions principle rests on independent grounding or reduces to existing dRL results.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and for identifying the need for explicit formal content to support the central claims. We agree that the supplied material (the abstract) does not contain the definitions, relations, or examples referenced in the abstract, and we will revise the manuscript to include them.

read point-by-point responses

  1. Referee: The abstract asserts that dRL supplies a uniform representation for refactorings (including auxiliary-variable cases) while simultaneously referring to properties and the original/refactored relation, yet no definitions of the relevant dRL propositions, refinement relations, or proof rules appear in the supplied material. Without these, the central uniformity and proof-transfer claims cannot be verified and remain load-bearing for the entire contribution.

    Authors: We acknowledge the validity of this comment. The supplied material consists only of the abstract, which summarizes the contribution without providing the formal definitions of the dRL propositions, refinement relations, or proof rules. In the revised manuscript we will add these definitions in the main sections to enable verification of the uniformity and proof-transfer claims. revision: yes

  2. Referee: No concrete example, derivation, or proof sketch is supplied to illustrate how a refactoring proposition is formed, how proof transfer occurs, or how automation or modularity is achieved. This absence prevents assessment of whether the refactoring-as-propositions principle rests on independent grounding or reduces to existing dRL results.

    Authors: We agree that the supplied material contains no concrete example, derivation, or proof sketch. The revised version will incorporate a concrete example together with a derivation and proof sketch demonstrating formation of a refactoring proposition, the proof-transfer mechanism, and the relation to prior dRL results. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper presents the refactoring-as-propositions principle as a method built on differential refinement logic (dRL) for proving preservation of properties under refactorings, including auxiliary variable introductions. The abstract and supplied material describe this as a uniform representation allowing simultaneous reference to system properties and original/refactored relations, with proofs that can be automated or reduced to local changes. No equations, definitions, or derivation steps are exhibited that reduce a claimed prediction or result to its inputs by construction, nor any load-bearing self-citation chain where the central claim collapses to an unverified prior result. dRL is treated as an established external logic providing the necessary expressiveness, making the contribution self-contained rather than circular. The uniformity and modularity claims rest on the logic's features rather than re-deriving them from the present work's outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

Only abstract available; ledger populated from claims in the abstract. Full paper may list additional axioms from dRL or free parameters in the refinement relations.

axioms (1)
  • domain assumption Differential refinement logic can simultaneously express system properties and refinement relations between original and modified hybrid systems.
    Stated as the foundation for representing refactorings as propositions.
invented entities (1)
  • refactoring-as-propositions principle no independent evidence
    purpose: Represent refactorings as propositions to enable proof transfer for property preservation.
    New framing introduced to organize the refactoring method.

pith-pipeline@v0.9.1-grok · 5683 in / 1115 out tokens · 32465 ms · 2026-06-30T19:28:03.737336+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

25 extracted references · 18 canonical work pages

  1. [1]

    Cambridge University Press (2010).https://doi.org/10.1017/CBO9781139195881

    Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010).https://doi.org/10.1017/CBO9781139195881

    work page doi:10.1017/cbo9781139195881 2010

  2. [2]

    Abrial, J., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf.12(6), 447–466 (2010).https://doi.org/10.1007/ S10009-010-0145-Y

    2010

  3. [3]

    In: Ab- stract State Machines, Alloy, B, VDM, and Z - Third International Confer- ence, ABZ 2012, Pisa, Italy, June 18-21, 2012

    Abrial, J., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: Ab- stract State Machines, Alloy, B, VDM, and Z - Third International Confer- ence, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings. pp. 178–193 (2012). https://doi.org/10.1007/978-3-642-30885-7_13,https://doi.org/10.1007/ 978-3-642-30885-7_13

    work page doi:10.1007/978-3-642-30885-7_13 2012

  4. [4]

    In: Raschke, A., Méry, D., Houdek, F

    Afendi, M., Laleau, R., Mammar, A.: Modelling hybrid programs with Event-B. In: Raschke, A., Méry, D., Houdek, F. (eds.) Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceed- ings. LNCS, vol. 12071, pp. 139–154. Springer (2020).https://doi.org/10.1007/ 978-3-030-48077-6_10

    2020

  5. [5]

    In: Abstract State Machines, Alloy, B, VDM, and Z - Third International Confer- ence, ABZ 2012, Pisa, Italy, June 18-21, 2012

    Banach, R., Zhu, H., Su, W., Wu, X.: Continuous behaviour in Event-B: A sketch. In: Abstract State Machines, Alloy, B, VDM, and Z - Third International Confer- ence, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings. pp. 349–352 (2012). https://doi.org/10.1007/978-3-642-30885-7_29,https://doi.org/10.1007/ 978-3-642-30885-7_29

    work page doi:10.1007/978-3-642-30885-7_29 2012

  6. [6]

    In: Pientka, B., Tinelli, C

    Brieger, M., Mitsch, S., Platzer, A.: Uniform substitution for dynamic logic with communicating hybrid programs. In: Pientka, B., Tinelli, C. (eds.) CADE. LNCS, vol. 14132, pp. 96–115. Springer (2023).https://doi.org/10.1007/ 978-3-031-38499-8_6

    2023

  7. [7]

    (eds.) Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday

    Butler,M.J.,Maamria,I.:PracticaltheoryextensioninEvent-B.In:Liu,Z.,Wood- cock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday. LNCS, vol. 8051, pp. 67–81. Springer (2013).https://doi.org/10.1007/978-3-642-39698-4_5

    work page doi:10.1007/978-3-642-39698-4_5 2013

  8. [8]

    Dupont, G., Ameur, Y.A., Pantel, M., Singh, N.K.: Proof-based approach to hybrid systemsdevelopment:DynamiclogicandEvent-B.In:AbstractStateMachines,Al- loy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings. pp. 155–170 (2018).https://doi.org/10.1007/ 978-3-319-91271-4_11,https://doi.org/10.1007/978-...

    work page doi:10.1007/978-3-319-91271-4_11 2018

  9. [9]

    In: 2019 International Sym- posiumonTheoreticalAspectsofSoftwareEngineering,TASE2019,Guilin,China, July 29-31, 2019

    Dupont, G., Ameur, Y.A., Pantel, M., Singh, N.K.: Handling refinement of contin- uous behaviors: A proof based approach with Event-B. In: 2019 International Sym- posiumonTheoreticalAspectsofSoftwareEngineering,TASE2019,Guilin,China, July 29-31, 2019. pp. 9–16 (2019).https://doi.org/10.1109/TASE.2019.00-25 Refactoring-as-Propositions 17

    work page doi:10.1109/tase.2019.00-25 2019

  10. [10]

    In: Ayala-Rincón, M., Muñoz, C.A

    Fulton, N., Mitsch, S., Bohrer, B., Platzer, A.: Bellerophon: Tactical theorem proving for hybrid systems. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP. LNCS, vol. 10499, pp. 207–224. Springer (2017).https://doi.org/10.1007/ 978-3-319-66107-0_14

    2017

  11. [11]

    In: Felty, A., Middel- dorp, A

    Fulton, N., Mitsch, S., Quesel, J.D., Völp, M., Platzer, A.: KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In: Felty, A., Middel- dorp, A. (eds.) CADE. LNCS, vol. 9195, pp. 527–538. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-21401-6_36

    work page doi:10.1007/978-3-319-21401-6_36 2015

  12. [12]

    (eds.): Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

    Grohe, M., Koskinen, E., Shankar, N. (eds.): Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. ACM, New York (2016)

    2016

  13. [13]

    In: Baier, C., Tinelli, C

    Jeannin, J., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne col- lision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS. LNCS, vol. 9035, pp. 21–36. Springer (2015).https://doi.org/10.1007/978-3-662-46681-0_2

    work page doi:10.1007/978-3-662-46681-0_2 2015

  14. [14]

    ACM Trans

    Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst.19(3), 427–443 (1997).https://doi.org/10.1145/256167.256195

    work page doi:10.1145/256167.256195 1997

  15. [15]

    In: Grohe et al

    Loos, S.M., Platzer, A.: Differential refinement logic. In: Grohe et al. [12], pp. 505–514.https://doi.org/10.1145/2933575.2934555

    work page doi:10.1145/2933575.2934555

  16. [16]

    In: 17th International Conference on Application of Concurrency to System Design, ACSD 2017, Zaragoza, Spain, June 25-30, 2017

    Lunel, S., Boyer, B., Talpin, J.: Compositional proofs in differential dynamic logic dl. In: 17th International Conference on Application of Concurrency to System Design, ACSD 2017, Zaragoza, Spain, June 25-30, 2017. pp. 19–28 (2017).https: //doi.org/10.1109/ACSD.2017.16,https://doi.org/10.1109/ACSD.2017.16

    work page doi:10.1109/acsd.2017.16 2017

  17. [17]

    In: Jones, C.B., Pihlajasaari, P., Sun, J

    Mitsch, S., Quesel, J.D., Platzer, A.: Refactoring, refinement, and reasoning: A logical characterization for hybrid systems. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM. LNCS, vol. 8442, pp. 481–496. Springer (2014).https://doi.org/ 10.1007/978-3-319-06410-9_33

    work page doi:10.1007/978-3-319-06410-9_33 2014

  18. [18]

    In: LICS

    Platzer, A.: Logics of dynamical systems. In: LICS. pp. 13–24. IEEE, Los Alamitos (2012).https://doi.org/10.1109/LICS.2012.13

    work page doi:10.1109/lics.2012.13 2012

  19. [19]

    Platzer, A.: A complete uniform substitution calculus for differential dy- namic logic. J. Autom. Reas.59(2), 219–265 (2017).https://doi.org/10.1007/ s10817-016-9385-1

    2017

  20. [20]

    In: Fontaine, P

    Platzer, A.: Uniform substitution at one fell swoop. In: Fontaine, P. (ed.) CADE. LNCS, vol. 11716, pp. 425–441. Springer (2019).https://doi.org/10.1007/ 978-3-030-29436-6_25

    2019

  21. [21]

    Platzer, A.: Hybrid dynamical systems logic and its refinements. Sci. Comput. Program.239, 103179 (2025).https://doi.org/10.1016/J.SCICO.2024.103179

    work page doi:10.1016/j.scico.2024.103179 2025

  22. [22]

    In: Dawar, A., Grädel, E

    Platzer, A., Tan, Y.K.: Differential equation axiomatization: The impressive power of differential ghosts. In: Dawar, A., Grädel, E. (eds.) LICS. pp. 819–828. ACM, New York (2018).https://doi.org/10.1145/3209108.3209147

    work page doi:10.1145/3209108.3209147 2018

  23. [23]

    In: Benzmüller, C., Heule, M.J., Schmidt, R.A

    Prebet, E., Platzer, A.: Uniform substitution for differential refinement logic. In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds.) IJCAR. LNCS, vol. 14740, pp. 196–215. Springer (2024).https://doi.org/10.1007/978-3-031-63501-4_11

    work page doi:10.1007/978-3-031-63501-4_11 2024

  24. [24]

    org/10.5281/zenodo.20142337,https://doi.org/10.5281/zenodo.20142337

    Prebet,E.,Platzer,A.:Refactoring-as-Propositions:1.0(May2026).https://doi. org/10.5281/zenodo.20142337,https://doi.org/10.5281/zenodo.20142337

    work page doi:10.5281/zenodo.20142337

  25. [25]

    1016/J.SCICO.2014.04.015,https://doi.org/10.1016/j.scico.2014.04.015 18 E

    Su, W., Abrial, J., Zhu, H.: Formalizing hybrid systems with Event-B and the Rodinplatform.Sci.Comput.Program.94,164–202(2014).https://doi.org/10. 1016/J.SCICO.2014.04.015,https://doi.org/10.1016/j.scico.2014.04.015 18 E. Prebet, A. Platzer A Additional Rules and Axioms used (:∗merge)x:=∗; ?p(x);x:=∗=x:=∗; ?∃y p(y) (=)a=b↔a≤b∧b≤a (MP) ϕ→ψ ϕ ψ (→2↔) ⊢ϕ↔ψ ⊢...

    work page doi:10.1016/j.scico.2014.04.015 2014