Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913129695281152 |
|---|---|
| author | Prebet, Enguerrand Platzer, André |
| author_facet | Prebet, Enguerrand Platzer, André |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_15001 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements Prebet, Enguerrand Platzer, André Logic in Computer Science F.3.1; F.4.1; D.2.4 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. |
| title | Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements |
| topic | Logic in Computer Science F.3.1; F.4.1; D.2.4 |
| url | https://arxiv.org/abs/2605.15001 |