Isabelle Sagot
email: isabelle.sagot@ibgc.cnrs.fr

Damien Laporte

Quiescence

AN INDIVIDUAL JOURNEY

Keywords: Quiescence, aging, micro-environment, G0, cell cycle

Quiescence is operationally characterized as a temporary and reversible proliferation arrest. There are many preconceived ideas about quiescence, quiescent cells being generally viewed as insignificant sleeping G1 cells. In fact, quiescence is central for organism physiology and its dysregulation involved in many pathologies. The quiescent state encompasses very diverse cellular situations depending on the cell type and its environment. This diversity challenges not only quiescence uniformity but also the universality of the molecular mechanisms beyond quiescence regulation. In this miniperspective, we discuss recent advances in the concept of quiescence, and illustrate that this multifaceted cellular state is gaining increasing attention in many field of biology.

Introduction

Unlike cell proliferation, cellular quiescence is often ill defined, considered as an inactive default state, and its biological relevance poorly acknowledged. However, an increasing amount of literature reveals that quiescence is central in many biological processes including major human diseases. In fact, quiescence is captivating, as it is diverse, multifaceted, and far from being a "sleeping" cellular state.

When speaking about cellular quiescence, it is crucial to define precisely what we are talking about. Quiescence is operationally defined as a temporary and reversible proliferation arrest, but conceptually, the difficulties arise from the rather loose notions of temporality and reversibility. First, one can wonder when does a cell that has ceased dividing should be considered as a bona fide quiescent cell? Although relevant, this question is probably not the way we should think about quiescence establishment, as quiescence entry is not a question of time but rather comes with specific molecular and cellular remodelling, that may even occur before cell proliferation cessation (see below). Second, a categorization based on reversibility separates quiescent cellscells that keep their capacities to re-enter the cell cycle-, from senescent cells -cells that will never re-proliferate [START_REF] Terzi | The cell fate: senescence or quiescence[END_REF]). Yet, although this partitioning is practically helpful, it may be too simplistic. As examples, terminally differentiated neurons are in an apparently permanent cell cycle arrest, but can eventually reproliferate following very particular stimulations [START_REF] Sun | States of G0 and the proliferation-quiescence decision in cells, tissues and during development[END_REF]. Similarly, viable but non-culturable micro-organisms theoretically fall in the senescent cell category, but it is just because we have not found the way to make them divide [START_REF] Oliver | The viable but nonculturable state in bacteria[END_REF]. On the other side of the edge, quiescent cells face the damaging effects of age and with time, may lose their proliferation capacities and become senescent [START_REF] Marthandan | Long-term quiescent fibroblast cells transit into senescence[END_REF]. Thus, the quiescence boundaries are floating.

In addition to these semantic issues, diverse forms of quiescence can be recognized.

On the one hand, quiescence induced by macro-or micro-environmental conditions can theoretically be separated from quiescence that is coupled to differentiation as part of a programmed developmental plan (O 'Farrell 2011;[START_REF] Fiore | Sleeping Beauty and the Microenvironment Enchantment: Microenvironmental Regulation of the Proliferation-Quiescence Decision in Normal Tissues and in Cancer Development[END_REF]. On the other hand, various quiescence "degree" can be ascribed depending on cell's "activities". For example, upon quiescence entry, primary human fibroblasts continue to exhibit high flux in several metabolic pathways [START_REF] Lemons | Quiescent fibroblasts exhibit high metabolic activity[END_REF][START_REF] Valcourt | Staying alive: metabolic adaptations to quiescence[END_REF]) while other cells drastically reduced their overall metabolism and enter dormancy, a sort of extreme form of quiescence. Dormancy has been brilliantly discussed for unicellular organisms [START_REF] Lewis | Persister cells, dormancy and infectious disease[END_REF][START_REF] Jones | Dormancy contributes to the maintenance of microbial diversity[END_REF][START_REF] Rittershaus | The normalcy of dormancy: common themes in microbial quiescence[END_REF]) and plants [START_REF] Considine | On the language and physiology of dormancy and quiescence in plants[END_REF][START_REF] Velappan | Cell cycle arrest in plants: what distinguishes quiescence, dormancy and differentiated G1?[END_REF]). Yet, while it is easy to acknowledge that spores are dormant since they undergo massive morphological changes [START_REF] Huang | Sporulation: how to survive on planet Earth (and beyond)[END_REF], this particular quiescent status is more debated in animals in which the frontiers of dormancy are more subjective [START_REF] Rittershaus | The normalcy of dormancy: common themes in microbial quiescence[END_REF][START_REF] Rocheteau | Dormancy and quiescence of skeletal muscle stem cells[END_REF]. In sum, quiescence encompasses an infinite number of cellular situations depending on both the cell type and the environmental niche. This heterogeneity challenges the universality of molecular processes beyond quiescence establishment, maintenance and exit. Nevertheless, once the complexity of quiescence acknowledged, increasing evidences testify that quiescence is not a "frozen" default G1 state and that this cellular state is at the heart of most physiological and pathological biological processes.

Quiescence is not an anecdotic cellular state.

In the wild, quiescent micro-organisms are found in most ecosystems, from the human gut to soils or deep oceans. When microbes face environmental conditions that are unfavorable to division, they may adopt different strategies to persist in a quiescent state for months or even years [START_REF] Corper | The viability and virulence of old cultures of tuercule bacilli[END_REF]. These "persisters" have been shown to be crucial not only to preserve biodiversity by limiting inter-species competition, but also for evolution [START_REF] Jones | Dormancy contributes to the maintenance of microbial diversity[END_REF][START_REF] Shoemaker | Evolution with a seed bank: The population genetic consequences of microbial dormancy[END_REF]. Because they are non-dividing and therefore insensitive to many antibiotics, these quiescent cells are also a major threat for human health [START_REF] Lewis | Persister cells, dormancy and infectious disease[END_REF][START_REF] Jones | Dormancy contributes to the maintenance of microbial diversity[END_REF][START_REF] Bojsen | Persistence and drug tolerance in pathogenic yeast[END_REF]. The evolutionary success of unicellular species is related to their ability to sustain periods of nutrient starvation. Throughout evolution, the appearance of multicellular organisms is closely associated with the acquisition of the capacity to enter quiescence (O 'Farrell 2011), even in a context in which cells are bathed in a nutrient-rich environment. In complex organisms, proliferation cessation at the right places and times is critical during development (O 'Farrell 2011;[START_REF] Sun | States of G0 and the proliferation-quiescence decision in cells, tissues and during development[END_REF]. In adults, many cells within tissues are quiescent, but the archetype of quiescent cells is undoubtedly stem cells. A controlled balance between proliferation and quiescence is crucial for regenerating tissues after injuries, for hematopoiesis, immune response, renewal of epithelia, etc… and therefore for the entire body maintenance [START_REF] Morrison | Stem cells and niches: mechanisms that promote stem cell maintenance throughout life[END_REF][START_REF] Farrell | Quiescence: early evolutionary origins and universality do not imply uniformity[END_REF][START_REF] Chakkalakal | The aged niche disrupts muscle stem cell quiescence[END_REF][START_REF] Rumman | Concise Review: Quiescence in Adult Stem Cells: Biological Significance and Relevance to Tissue Regeneration[END_REF][START_REF] Matson | Cell cycle proliferation decisions: the impact of single cell analyses[END_REF][START_REF] Fiore | Sleeping Beauty and the Microenvironment Enchantment: Microenvironmental Regulation of the Proliferation-Quiescence Decision in Normal Tissues and in Cancer Development[END_REF]. Moreover, quiescence establishment and exit, through the regulation of cell proliferation, have to be tightly controlled to avoid pathological situations including stem cell depletion and tumorigenesis [START_REF] Orford | Deconstructing stem cell self-renewal: genetic insights into cell-cycle regulation[END_REF][START_REF] Farrell | Quiescence: early evolutionary origins and universality do not imply uniformity[END_REF][START_REF] Cheung | Molecular regulation of stem cell quiescence[END_REF][START_REF] Dhawan | Decoding the stem cell quiescence cycle--lessons from yeast for regenerative biology[END_REF]. Interestingly, more and more evidences argue that microenvironment -both its composition and physical properties -plays a central role in regulating quiescence [START_REF] Linde | The Relationship Between Dormant Cancer Cells and Their Microenvironment[END_REF][START_REF] Fiore | Sleeping Beauty and the Microenvironment Enchantment: Microenvironmental Regulation of the Proliferation-Quiescence Decision in Normal Tissues and in Cancer Development[END_REF]. This is particularly true in the case of disseminated tumor cells that persist far from the primary tumor as undetectable quiescent individual cancer cells, the awakening of these malignant cells being thought to be the major cause of cancer recurrence (Aguirre-Ghiso et al. 2013; [START_REF] Sosa | Mechanisms of disseminated cancer cell dormancy: an awakening field[END_REF][START_REF] Linde | The Relationship Between Dormant Cancer Cells and Their Microenvironment[END_REF][START_REF] Fiore | Sleeping Beauty and the Microenvironment Enchantment: Microenvironmental Regulation of the Proliferation-Quiescence Decision in Normal Tissues and in Cancer Development[END_REF]). In addition to disseminated tumor cells, non-proliferating cancer cells -cancer stem cells -do exist within tumors and as such, resist to conventional anti-proliferative drug treatments [START_REF] Chen | Cancer Stem Cell Quiescence and Plasticity as Major Challenges in Cancer Therapy[END_REF][START_REF] Fujimaki | Crack the state of silence: Tune the depth of cellular quiescence for cancer therapy[END_REF][START_REF] Vallette | Dormant, quiescent, tolerant and persister cells: four synonyms for the same target in cancer[END_REF]. Several strategies are currently under investigation to avoid cancer relapse and resistance, such as locking quiescent cancer cells in a non-proliferative state or forcing them to divide in the presence of chemotherapeutic agents [START_REF] Chen | Cancer Stem Cell Quiescence and Plasticity as Major Challenges in Cancer Therapy[END_REF]). Thus, it urges to decrypt mechanisms beyond both quiescence regulation in healthy tissues and quiescence dysfunction in human pathologies.

Quiescence establishment is not a passive arrest in G1.

Quiescence establishment is often considered as a passive proliferation arrest at the restriction point in the G1 phase of the cell cycle. While the majority of quiescent cells do have a G1 DNA content, there are many examples of plants and animal cells that undergo endo-replication prior to quiescence entry and are therefore polyploidy [START_REF] Sun | States of G0 and the proliferation-quiescence decision in cells, tissues and during development[END_REF]. Further, quiescent cells are not all necessarily arrested at the same "point" in G1 [START_REF] Cooper | Reappraisal of serum starvation, the restriction point, G0, and G1 phase arrest points[END_REF][START_REF] Yao | Modelling mammalian cellular quiescence[END_REF]) and several yeast species [START_REF] Costello | Fission yeast enters the stationary G0 state from either mitotic G1 or G2[END_REF][START_REF] Takeo | Unbudded G2 as well as G1 arrest in the stationary phase of the basidiomycetous yeast Cryptococcus neoformans[END_REF], stem cells (Sutcu and Ricchetti 2018) and cancer cells [START_REF] Drewinko | Cultured human tumour cells may be arrested in all stages of the cycle during stationary phase: demonstration of quiescent cells in G1, S and G2 phase[END_REF][START_REF] Mizrahi | Persistence to anti-cancer treatments in the stationary to proliferating transition[END_REF]) can be found quiescent in G2. In fact, S. cerevisiae and S. pombe can survive in quiescence when they are artificially arrested in other cell cycle phase than G1 [START_REF] Wei | Yeast cells can enter a quiescent state through G1, S, G2, or M phase of the cell cycle[END_REF][START_REF] Laporte | Metabolic status rather than cell cycle signals control quiescence entry and exit[END_REF]. Nonetheless, several studies point to many signaling molecules acting in G1 as regulator of quiescence. This includes the tumor suppressor p53 and Rb, the cyclin-dependent kinase inhibitors p21 and p27, and several transcription factors such as FoxO [START_REF] Cheung | Molecular regulation of stem cell quiescence[END_REF][START_REF] Rumman | Concise Review: Quiescence in Adult Stem Cells: Biological Significance and Relevance to Tissue Regeneration[END_REF][START_REF] Sun | States of G0 and the proliferation-quiescence decision in cells, tissues and during development[END_REF][START_REF] Matson | Cell cycle proliferation decisions: the impact of single cell analyses[END_REF][START_REF] Miles | A common strategy for initiating the transition from proliferation to quiescence[END_REF]). Yet, inactivation of these pathways does not necessarily hamper quiescence establishment [START_REF] Matson | Cell cycle proliferation decisions: the impact of single cell analyses[END_REF]. Importantly, an artificial prolonged G1 arrest does not recapitulate quiescence establishment both in yeast and mammals [START_REF] Coller | A new description of cellular quiescence[END_REF][START_REF] Laporte | Metabolic status rather than cell cycle signals control quiescence entry and exit[END_REF]. In fact, accumulating evidences indicate that quiescence establishment involves the active repression of G1 progression genes [START_REF] Litovchick | Evolutionarily conserved multisubunit RBL2/p130 and E2F4 protein complex represses human cell cycledependent genes in quiescence[END_REF][START_REF] Sang | Control of the reversibility of cellular quiescence by the transcriptional repressor HES1[END_REF][START_REF] Yao | Modelling mammalian cellular quiescence[END_REF][START_REF] Matson | Cell cycle proliferation decisions: the impact of single cell analyses[END_REF] Cook 2017) and the expression of genes which signature vary depending on the signal that has triggered quiescence entry [START_REF] Coller | A new description of cellular quiescence[END_REF][START_REF] Klosinska | Yeast cells can access distinct quiescent states[END_REF]. Further, expression of particular miRNAs, the RNA interference machinery, specific histone marks and telomere rearrangements have been shown to regulate quiescence [START_REF] Cheung | Molecular regulation of stem cell quiescence[END_REF][START_REF] Roche | Transcriptional reprogramming in cellular quiescence[END_REF][START_REF] Maestroni | STEEx, a boundary between the world of quiescence and the vegetative cycle[END_REF], suggesting that this cellular fate is actively established and maintained. In addition, quiescence entry is accompanied by many specific remodelling, including chromatin reorganization, protein re-localization and cytoskeletal re-arrangements [START_REF] Sagot | The cell biology of quiescent yeast: a diversity of individual scenario[END_REF].

These large-scale cellular manoeuvres may be a way to avoid the damaging effects of age or to improve the fitness of quiescence exit.

Finally, studies in mammals suggest that the decision to enter quiescence is taken prior to the proliferation arrest in G1, in the G2 phase of the previous cell cycle. This forecast cell fate involves a bifurcation in the levels of Cdk2 activity and a Rb-E2F bistable switch [START_REF] Hitomi | Cyclin D1 production in cycling cells depends on ras in a cell-cycle-specific manner[END_REF][START_REF] Chassot | Confluence-induced cell cycle exit involves pre-mitotic CDK inhibition by p27(Kip1) and cyclin D1 downregulation[END_REF][START_REF] Spencer | The proliferation-quiescence decision is controlled by a bifurcation in CDK2 activity at mitotic exit[END_REF][START_REF] Naetar | PP2A-mediated regulation of Ras signaling in G2 is essential for stable quiescence and normal G1 length[END_REF][START_REF] Dhawan | Decoding the stem cell quiescence cycle--lessons from yeast for regenerative biology[END_REF][START_REF] Sun | States of G0 and the proliferation-quiescence decision in cells, tissues and during development[END_REF][START_REF] Matson | Cell cycle proliferation decisions: the impact of single cell analyses[END_REF]. Interestingly, in yeast, the decision seems to be made several cell cycles before proliferation cessation [START_REF] Lillie | Reserve carbohydrate metabolism in Saccharomyces cerevisiae: responses to nutrient limitation[END_REF][START_REF] Zhang | Starvation signals in yeast are integrated to coordinate metabolic reprogramming and stress response to ensure longevity[END_REF][START_REF] Argüello-Miranda | Integration of Multiple Metabolic Signals Determines Cell Fate Prior to Commitment[END_REF]. Therefore, quiescence establishment is a multifaceted anticipated process for which a G1 arrest is not mandatory, thereby questioning the use of the term "G0".

Quiescence is not a "frozen" cellular state

Are all quiescent cells "frozen"? As stated above, depending on the cell type, quiescent cells metabolic activities drastically vary. Although it may be slowed down, a minimal rate of protein synthesis is required for survival in quiescence. Besides, an increased mRNA stability has been observed in many quiescent cell types [START_REF] Gray | Sleeping beauty": quiescence in Saccharomyces cerevisiae[END_REF][START_REF] Valcourt | Staying alive: metabolic adaptations to quiescence[END_REF][START_REF] Rittershaus | The normalcy of dormancy: common themes in microbial quiescence[END_REF]. Quiescent cells also preserve both membrane potentials and energy production, the maintenance of ATP synthesis, either by respiration or fermentation, being essential to avoid cell death [START_REF] Rittershaus | The normalcy of dormancy: common themes in microbial quiescence[END_REF]. Further, quiescence is not necessarily associated to a general slowdown of all metabolic fluxes [START_REF] Sauer | Metabolic flux ratio analysis of genetic and environmental modulations of Escherichia coli central carbon metabolism[END_REF][START_REF] Lemons | Quiescent fibroblasts exhibit high metabolic activity[END_REF][START_REF] Klosinska | Yeast cells can access distinct quiescent states[END_REF][START_REF] Valcourt | Staying alive: metabolic adaptations to quiescence[END_REF][START_REF] Rittershaus | The normalcy of dormancy: common themes in microbial quiescence[END_REF], some specific pathways being more active in quiescent cells than in their proliferating counterpart [START_REF] Lemons | Quiescent fibroblasts exhibit high metabolic activity[END_REF][START_REF] Chen | Quiescent fibroblasts are more active in mounting robust inflammatory responses than proliferative fibroblasts[END_REF]. Hence, quiescent cells are not all asleep.

In fact, many quiescent cells seem to be poised, ready to re-enter the cell cycle the more efficiently as possible [START_REF] Cheung | Molecular regulation of stem cell quiescence[END_REF]. In quiescent S. cerevisiae, the RNA polymerase II is stalled onto specific promoters, ready to fire genes required for the early steps of G1/S progression [START_REF] Radonjic | Genome-wide analyses reveal RNA polymerase II located upstream of genes poised for rapid response upon S. cerevisiae stationary phase exit[END_REF]. A similar mechanism may exist in stem cells, in which epigenetic histone marks could be functionally important for cell cycle re-entry [START_REF] Cheung | Molecular regulation of stem cell quiescence[END_REF]. Moreover, some transcription factors and several quiescence specific cellular reorganization such as the formation of proteasome storage granules and stable microtubule bundles are critical for quiescence exit [START_REF] Sagot | The cell biology of quiescent yeast: a diversity of individual scenario[END_REF][START_REF] Kuang | Stress response factors drive regrowth of quiescent cells[END_REF]). More generally, cellular machineries essential for proliferation such as cytoskeletons or macromolecular complexes may be stored in quiescent cells as immediately mobilizable reservoir [START_REF] Sagot | The cell biology of quiescent yeast: a diversity of individual scenario[END_REF]. Further, difference in responsiveness have been observed in both yeast and several mammalians quiescent cells, including stem cells. Indeed, within a clonal cell population, individual quiescent cells can exhibit significantly different swiftness in re-entering proliferation [START_REF] Rodgers | mTORC1 controls the adaptive transition of quiescent stem cells from G0 to G(Alert)[END_REF][START_REF] Dhawan | Decoding the stem cell quiescence cycle--lessons from yeast for regenerative biology[END_REF][START_REF] Tierney | Satellite Cell Heterogeneity in Skeletal Muscle Homeostasis[END_REF][START_REF] Wang | Exit from quiescence displays a memory of cell growth and division[END_REF][START_REF] Laporte | Yeast quiescence exit swiftness is influenced by cell volume and chronological age[END_REF]). Finally and importantly, it has been proposed that quiescence duration influences individual quiescent cell properties and that young quiescent cells do not have the same features and abilities that cells that have been quiescent for longer period. In yeast and fibroblast, this "deepening" of quiescence has been shown to negatively influence quiescence exit efficiency [START_REF] Yao | Modelling mammalian cellular quiescence[END_REF][START_REF] Wang | Exit from quiescence displays a memory of cell growth and division[END_REF][START_REF] Kwon | Controlling Depth of Cellular Quiescence by an Rb-E2F Network Switch[END_REF][START_REF] Laporte | Yeast quiescence exit swiftness is influenced by cell volume and chronological age[END_REF]. Thus, quiescent cell properties change with time.

As a conclusion, quiescent cells properties are very different depending on the cell type, its environment, and the time spend in this non-proliferating state. Even clonal cell population in a given niche should be considered as a sum of heterogeneous individualities. It may be unrealistic to believe that universal properties shared by all quiescent cells could exist and that the molecular mechanisms beyond quiescence regulation are all evolutionary conserved. Yet, quiescence in its biological significance, its diversity and its complexity is a fascinating cellular state, and we have just uncovered the very tip of the iceberg. Many more is to come…

Acknowledgments

We express our profound gratitude to B. Daignan-Fornier for precious discussions and comments on this manuscript. DL and IS are supported by the University of Bordeaux and the Centre National de la Recherche Scientifique.


Demba Boubacar
email: boubacar.sall@lip6.fr

Frédéric Sall

Emmanuel Peschanski
email: frederic.peschanski@lip6.fr

Chailloux

A Mechanized Theory of Program Refinement

Keywords: Stepwise refinement, Program verification, Predicative programming, Correctness by construction, Type theory, Proof assistant, Coq

We present a mechanized theory of program refinement that allows for the stepwise development of imperative programs in the Coq proof assistant. We formalize a design language with support for gradual refinement and a calculus which enforces correctness-by-construction. A notion of program design captures the hierarchy of refinement steps resulting from a development. The underlying theory follows the predicative programming paradigm where programs and specifications are both easily expressed as predicates, which fit naturally in the dependent type theory of the proof assistant.

Introduction

Program development by stepwise refinement [START_REF] Dijkstra | Notes on structured programming[END_REF][START_REF] Spivey | The Z notation[END_REF][START_REF] Wirth | Program development by stepwise refinement[END_REF] is inherently an interactive activity alternating programming steps and proof steps feeding back on each other. It therefore makes sense to perform refinement steps within an interactive proof assistant whose very purpose is to help in specification, proof composition and mechanical proof verification. This however requires that a theory of program refinement be embedded in the formalism of the proof assistant (p.a.). Most theories of refinement fall in two groups. The theories (e.g. [START_REF] Frappier | A relational calculus for program construction by parts[END_REF][START_REF] Mili | A relational approach to the design of deterministic programs[END_REF]) in the first group are based upon the calculus of relations, and represent programs as well as specifications uniformly as set-theoretic relations on program states. In the second group, the theories (e.g. [START_REF] Morgan | The refinement calculus[END_REF][START_REF] Back | A calculus of refinements for program derivations[END_REF]) are underpinned by Hoare logic or the wp-calculus 1 . The view there is that programs relate sets of program states represented in logic as predicates, while specifications are pairs of predicates. In this paper, we investigate the predicative programming [START_REF] Hehner | Predicative programming part I[END_REF][START_REF] Sekerinski | A calculus for predicative programming[END_REF] approach to refinement which can be viewed as an expression of the relational point of view in predicative terms rather than in set theory. This investigation lead to the development of a mechanized theory of stepwise refinement towards imperative programs (similar to those studied in [START_REF] Morgan | The refinement calculus[END_REF]) in the realm of the Coq p.a. [START_REF] Team | The coq proof assistant[END_REF]. We have the following contributions.

Firstly, we formalize in type theory a language of stepwise program design, and a calculus which enforces correctness by construction. The language is an extension of a simple imperative language with assignment, sequence, if statements and iteration. The extension is to allow the expression of an hierarchy of refinement steps, each step associating a specification to an implementation. The calculus stems from a synthesis of ideas from predicative and relational theories of refinement. On the one hand, the relational point of view unifies the usual assertions (e.g. precondition, post-condition, invariant) under a single and more general notion of specification, hence simplifying the formulation of the theory. On the other hand, the predicative point of view makes it easier to write specifications and handle proof obligations (p.o.s).

Secondly, we uncover necessary and sufficient conditions for a while statement to refine a given specification. In particular, the loop body must be given an adequate relational specification. The advantage is that theses specifications are more flexible than invariants.

Finally, we have mechanized the aforementioned calculus as well as the underlying theory in the Coq p.a. so that the declaration of a refinement step automatically triggers the generation of p.o.s (in the language of the p.a.) to ensure the correctness of the refinement. All the artifacts presented in the paper (definitions and theorem statements), as well as all the proofs, have been formalized in about 4000 lines of Coq script and made available in a companion repository 2 . This framework thus permits certified imperative program design by gradual refinement, and demonstrates that, in terms of mechanized semantics in type theory, the relational point of view is a viable alternative to Hoare-logic style semantics. Moreover, the Coq p.a. provides a full blown functional language to write specifications with the benefit of type checking, type inference and parametric polymorphism for free.

The outline of the paper is as follows. In Section 2 we give an overview of program development by stepwise refinement in our proposed framework. In Section 3 we introduce the language of program designs, we describe the rules of the calculus, and we formulate the corresponding correctness theorem. In Section 4 we formalize the semantics of our language, we define the refinement relation based on this semantics, and we justify the design rules introduced in Section 3. In Section 5 we turn our attention to making the framework more practical by applying some automatic simplifications to the p.o.s. A discussion of related work and the conclusion follow.

An overview of stepwise program design

To give an overview of our framework as experienced by the user, we use a classical example: the (integer) square root computation. We begin by declaring the following abstract definition of the square root computation:

Program Definition Sqrt := r 2 ≤ x < (r + 1) 2 x .
With the Definition keyword we have named our computation Sqrt, and declared its high level specification. The role of the Program keyword will be clarified shortly, it has to do with the handling of p.o.s. Most specifications we will write are akin to before-after predicates which describe the relation between the initial state and the final state of a program. We use the usual convention that variables are primed to mean their value after execution, and unprimed to mean their value before execution. The specification3 of the square root computation reads as follows: from the initial value of variable x we aim to compute its square root and make the result available as the final value of r (denoted r ). Additionally, the value of x is required to remain unchanged. Our objective is to elaborate, incrementally, a program to fulfill this specification. Once we have decided on a more precise implementation, we open braces to write this implementation. In our example, this first refinement step leads to the following situation:

(1) Program Definition Sqrt := r 2 ≤ x < (r + 1) 2 x { r := 0; h := x + 1; r 2 ≤ r 2 ≤ x < h 2 ≤ h 2 ∧ r + 1 = h x }.
Our initial specification has developed into a specified block [START_REF] Hehner | Specified blocks[END_REF] whose header is the initial specification. The body of the block introduces a new variable h so that [r..h] delimits the search space. The last statement specifies the search strategy we intend to implement, i.e. narrow the search space around x (first conjunct), up to the point where the initial specification is fulfilled (second conjunct). The notations being used to design the square root computation (e.g.

... {...}, ;) are syntactic sugar for invoking specific constructions rules defined in Section 3.2. These rules ensure the correctness of our design with respect to the semantics defined in Section 4. In particular the rules stipulate that to construct the specified block above, one must provide a proof that the body of the block refines (in the sense of Section 4.2) the header of the block. Thanks to the Program keyword we can mimic the construction of a specified block and let the p.a. save the p.o. corresponding to the missing proof for later. This p.o. is to be discharged separately so that our design is not cluttered with the details of the proofs. At this point, even though the p.a. has performed some type checking automatically, the Sqrt definition is not yet complete: for example it cannot be referred to in other definitions. To complete the definition, we must provide the missing proof by writing a proof script which is generally of the following form:

Next Obligation. t1. ... ti. nia. ... tj. ... t k . Qed.

The Next Obligation command is to fetch and display the next p.o. among those left to be discharged. The following sequence of t i commands invoke built-in proof tools called tactics, for example the nia tactic used to deal with non linear arithmetic is very helpful in our case. Finally, the Qed command instructs the p.a. to check our proof for validity. By repeating the process we have just described to make specifications more and more precise, we ultimately obtain the design of Listing 1.1 below after three more refinement steps (labeled (2), ( 3) and ( 4)).

(1) Program Definition Sqrt := r 2 ≤ x < (r + 1) 2 x { r := 0;

h := x + 1; (2) r 2 ≤ r 2 ≤ x < h 2 ≤ h 2 ∧ r + 1 = h x { while r + 1 = h do (3) r 2 ≤ r 2 ≤ x < h 2 ≤ h 2 ∧ (r < r ∨ h > h ) x { (4) r < m < h x,r,h { m := r + (h -r)/2 }; if m 2 ≤ x then r := m else h := m end } done }}.
Listing 1.1. The square root program design with refinement steps (1) to ( 4)

The second refinement step has consisted in deciding to implement the search strategy as a loop. The body of the loop required two more refinement steps (numbered (3) and ( 4)). An important remark is that all the successive steps are visible in the final design: one can imagine collapsing specified blocks showing only the associated specifications, or instead expanding blocks to dig into the implementation details. Once all p.o.s are discharged we have built an object carrying programming instructions, the design decisions (refinement steps) that lead to those instructions, and the proofs of correctness of all refinements. We call this object a program design. Keeping all refinement steps around is important because the corresponding design decisions tend to be lost as time passes, rendering program evolution ever more harder. Thanks to the proofs carried by the program design, our framework is able to assemble a global certificate of design correctness. To assemble such a certificate we write the following script:

Definition sqrt proof := CbC.soundness Sqrt.
In other words, the sqrt proof term results from applying the soundness theorem of our design rules (the Cbc.soundness term) to the Sqrt design. This term is a proof that can be independently checked for validity. The soundness theorem of the design rules is formulated in Section 3. We refer the reader to the companion repository for a detailed example 4 of how the refinement process is carried out for the square root computation.

The calculus of program designs

In this section we formally present the calculus of program designs. We begin with the language of program designs. Then, we formulate the construction rules of the calculus whose purpose is to enforce correctness-by-construction.

Statement S ::= effect f (with the state transformer f :

T → T ) | R (specification statement with R : T → T → Prop) | S1 ; S2 (sequence) | if C then S1 else S2 endif (if statement with condition C : T → Prop 5 ) | S1 { S2 } (specified block with S1 block free) | while C do S done (iteration with condition C : T → Prop)
Fig. 1. The design language w.r.t. the type T of program states

The language of program designs

To design programs in the way described previously, we need a language with support for gradual refinement. Moreover, adhering to the correctness by construction [START_REF] Kourie | The Correctness-by-Construction Approach to Programming[END_REF] paradigm, our objective is to impose further restrictions so that only correct program designs can be constructed. The syntax of the core language we study is given in Figure 1. It is a very classical imperative language, close in spirit to the language studied in [START_REF] Morgan | The refinement calculus, and literate development[END_REF], but embedded in the Coq p.a. Since Coq is underpinned by a dependent type theory, type checking, type inference and parametric polymorphism are for free. In the p.a., the syntax is encoded as an inductive type implicitly parameterized by the type T of program states.

The statements of the language. Sequential composition as well as the statements related to the if and while keywords are self-explanatory. The effect statement reflects the notion of state transformation as a syntactic constructor. This provides a nice generalization of various kinds of effects. For example the skip instruction is defined as effect (λ s ⇒ s). Assignment statements are also derivable. For example, the assignment v := v + w for v and w variables of type Nat translates to effect (λ (v, w) ⇒ (v + w, w)) where T is Nat × Nat.

The R construct is a specification statement [START_REF] Morgan | The refinement calculus[END_REF]. It can be thought of as standing for a "program fragment yet to be implemented", or alternatively as a procedure call to a program specified by R. The notation ... is from [START_REF] Knuth | Literate programming[END_REF]. The encoding in Coq of before-after predicates is straightforward. For example λ (i i : nat) ⇒ i > i specifies a program that increases variable i. More generally, R designates a program P such that : (1) when started in state s the set of possible outputs of P is { s | R s s }, and (2) P terminates on input s exactly when (∃ s • R s s ) is true (i.e. the set of possible outputs is not empty). Non deterministic behavior is reflected by a number of possible outputs greater than one. Following [START_REF] Sekerinski | A calculus for predicative programming[END_REF], we equate abnormal termination in an error state with non termination, therefore abort ≡ λ (s s : T ) ⇒ False .

The specified block S 1 { S 2 } represents a pair of statements resulting from the refinement of S 1 by S 2 as explained in Section 2. This is the feature enabling gradual refinement. S 1 is called the abstraction of the block and S 2 is called the concretization. We assume that the abstraction S 1 does not itself contain specified blocks, we say that it is block free. Note that programming constructs

                       ϕ(effect f ) def = (effect f ) { (effect f ) } ϕ( R ) def = R { R } ϕ(S1;S2) def = ϕa(S1) ; ϕa(S2) { ϕc(S1) ; ϕc(S2) } ϕ(if C then S1 else S2 endif) def = if C then ϕa(S1) else ϕa(S2) endif { if C then ϕc(S1) else ϕc(S2) endif } ϕ(S1 { S2 }) def = S1 { ϕc(S2) } ϕ(while C do S done) def = if C then λ s s ⇒ [[ϕa(S)]] s s ∧ ¬C s endif { while C do ϕc(S) done } Fig. 2.
The design projection function ϕ are welcome in the abstraction of specified blocks. For example, the abstraction of a block can be of the if-then-else form. During program design, when we write S 1 { S 2 }, we record a design decision which communicates an abstract intent (S 1 ), and some (hopefully more concrete and correct) means of realizing it (S 2 ).

The ϕ projection function. We now define the projection function ϕ, which will be used in the formulation of the rules and properties of the calculus. The definition is given in Figure 2 above. From a statement S, ϕ computes an abstraction ϕ a (S), and a (generally distinct) concretization ϕ c (S), such that both statements are block free. We write ϕ(S) = ϕ a (S) { ϕ c (S) } to match the syntax of the language. For example, if we consider the program design of Listing 1.1, the corresponding abstraction is the outermost specification r 2 ≤ x < (r +1) 2

x , and the concretization is the statement resulting from the intermediate specifications (lines in blue labeled (1) up to (4)) being ignored.

ϕ is defined so that the effect and R statements are respectively their own abstraction. Concerning sequential composition and the if-the-else construct, ϕ simply extracts the (abstraction,concretization) pairs from the inner statements and combines them in parallel.

In the case of the specified block the corresponding abstraction is just S 1 by definition, and the concretization is the one of the body of the block.

The abstraction of a loop is constructed from the abstraction of its body, which therefore must be specified with care. We come back to this in Section 4.3.

The [[•]

] operator refers to the interpretation of statements as binary relations on program states. This interpretation is detailed in Section 4.1. To give an example, [[i := i + 1]] denotes the predicate i = i + 1 (encoded as (λ i i ⇒ i = i + 1) in the p.a.).

Actually we use ϕ a (S) to reason about S while abstracting away from implementation details, and we compute ϕ c (S) to get a block free statement which can be translated into a programming language provided S is precise enough (i.e. no specification statements among the leaves of the syntax tree). The calculus we

Design (effect f ) Design R Design S1 ∧ Design S2 Design S1;S2 Design S1 ∧ Design S2 Design (if C then S1 else S2 endif) Design S2 ∧ ϕa(S2) S1 Design (S1 { S2 }) Design S ∧ K;K K, with K def = (if C then ϕa(S) endif) ∧ well founded (λ s s ⇒ C s ∧ ([[ϕa(S)]] s s) ∧ C s)
Design (while C do S done) Fig. 3. The calculus of program designs define in Section 3.2 allows to characterize those statements S such that ϕ c (S) is indeed a refinement of ϕ a (S).

Enforcing correctness-by-construction

The usefulness of a program design rests upon the correctness of what this design communicates. In order to enforce design correctness, we restrict our language by imposing strict construction rules. We say that a program design S is correct if and only if the predicate Design S can be derived from the rules of Figure 3. The two basic instructions effect and R are, unsurprisingly, the axioms of the proof system. All the statements involved in the other compound instructions must already be correct designs. The rule for specified blocks involves the refinement relation . This relation will be formally defined in Section 4.2, but for now we describe it as follows: we say that S 2 S 1 if and only if every specification satisfied by S 1 is also satisfied by S 2 . In fact, when S 1 and S 2 are block free, our formalization allows to derive formally this description of refinement in terms of Hoare triples, i.e. we have established the following equivalence:

S 2 S 1 ↔ ∀ P Q • {P } S 1 {Q} → {P } S 2 {Q}
The requirements for a block S 1 { S 2 } to be a correct design are as follows. First, it must be the case that S 2 is a correct design, and moreover that ϕ a (S 2 ) refines S 1 . In the rule for specified blocks and while loops, we can abstract away from implementation details and only consider ϕ a (S) because we assume S to be a correct program design. The rule for while loops is more intricate. The requirement that K;K refines K is to ensure that K is a correct over-approximation of the loop's behavior. The well-foundedness requirement ensures as it is usually the case that the loop terminates on all inputs of interest. Ultimately, the central theorem of our proposed framework is the following one.

Theorem 1 (Correctness of program designs).

(soundness This theorem explains that whenever we are able to derive Design S for some program design, the associated concretization refines the associated abstraction. Clearly it is possible to have ϕ c (S) ϕ a (S) while Design S is not derivable. For example consider the following program design

) ∀ S • Design S → ϕ c (S) ϕ a (S) (completeness) ∀ S 1 S 2 • S 2 S 1 → ∃ S • Design S ∧ ϕ(S) = S 1 { S 2 } [[•]] : Statement → Spec [[effect f ]] def = λ s s ⇒ s = (f s) [[ R ]] def = R [[S1;S2]] def = [[S1]] [[S2]] [[if C then S1 else S2 endif]] def = [[S1]] C [[S2]] [[S1 { S2 }]] def = [[S2]] [[while C do S done]] def = lfp 6 (λ X ⇒ ([[S]] X ) C [[skip]])
S def = skip { λ s s ⇒ False { skip } }.
We have skip skip, and yet Design S cannot be derived. So as one would expect the design rules are not complete in the absolute sense. However they are complete in the weaker sense that for any concretization S 2 and abstraction S 1 such that S 2 S 1 , it is possible to come up with a correct design S whose associated concretization and abstraction are respectively S 2 and S 1 . When we complete a design, the soundness part of Theorem 1 allows to construct a tangible lambda term certifying that our design is indeed correct: this lambda term is the certificate of correctness we alluded to in Section 2. The completeness part of Theorem 1 reassures us that the design rules we restrict ourselves to use do not themselves restrict the kind of programs that can be obtained by applying these rules.

Predicative semantics and refinement relation

In this section we discuss the key properties justifying the design rules of our calculus. First we present the predicative interpretation of statements and define the refinement relation in terms of this interpretation. Then, we examine the particular case of loops.

Predicative semantics

Except for loops and specified blocks, our interpretation of statements as predicates corresponds to the predicative semantics of [START_REF] Sekerinski | A calculus for predicative programming[END_REF]. We denote by Spec the type of specifications, i.e. the type of binary relations on the type T of program states.

Spec def = T → T → Prop
The predicative interpretation of statements associates to each statement a specification of type Spec. This interpretation is inductively defined on the syntax of statements as indicated in Table 1 above.

State transformation, specification statements and specified blocks. The specification associated to (effect f ) explains that the after state is the image by f of the before state. The interpretation of R is just R since R is already a specification. For specified blocks, we choose the interpretation of the supposedly better implementation among the statements composing the block.

Alternative. The if-then-else statement denotes the specification described in Equation ( 1) below. Here, A and B are of type Spec and C has type T → Prop.

A C B def = λ (s s : T ) ⇒ C s ∧ (A s s ) ∨ ¬(C s) ∧ (B s s ) (1)
The notation used is borrowed from [START_REF] Hoare | Unifying theories of programming[END_REF], and expresses a selection between two specifications depending on C, i.e. either C is true ( ) of the input state and A is selected, or C is false ( ) of the input state and B is selected. Note that conditions C of the if and while statements send states to Prop rather than to bool.

The choice of Prop for the type Spec makes writing specifications easier because unlike bool, Prop is closed under universal and existential quantification. Once Prop is chosen for specifications, it makes sense for the sake of uniformity, to also choose Prop for conditions. For example, choosing bool for conditions would require reflecting bool in Prop to write Equation (1) above. As a consequence of choosing Prop, the decidability of the conditions is not enforced by typing. However, the predicative semantics of the if-then-else and while statements implicitly address this decidability issue since whenever such statements are defined on a state s, it follows that (C s ∨ ¬C s) is true.

Sequence. For sequential composition, we need a notion of composition for specifications. We define below the angelic and demonic composition of specifications.

Definition 1 (Sequential composition of specifications). Let S 1 and S 2 be of type Spec. The angelic and demonic composition operators are respectively defined as follows:

S 1 S 2 def = λ s s ⇒ ∃ s x • S 1 s s x ∧ S 2 s x s S 1 S 2 def = λ s s ⇒ (S 1 S 2 ) s s ∧ ∀ s x • S 1 s s x → ∃ s • S 2 s x s
Angelic composition is just relational composition. Demonic composition is relational composition further restricted to account for the fact that the interpretation of S 1 ; S 2 is defined only on those states s such that S 2 is defined for all possible outputs of S 1 on s. As an illustration of the difference between the two operators, consider the following example:

{(1, 2), (1, 3)} {(2, 4)} = {(1, 4)}, but {(1, 2), (1, 3)} {(2, 4)} = {}
We see that angelic composition does not properly capture the possibility of failure because the input 1 should not be present in the domain of the composition since it may cause an error if the output is 3. Therefore, as in [START_REF] Frappier | A relational calculus for program construction by parts[END_REF], we use demonic composition [START_REF] Berghammer | Relational algebraic semantics of deterministic and nondeterministic programs[END_REF][START_REF] Backhouse | Demonic operators and monotype factors[END_REF] to formalize the sequential composition of specifications. Consequently, the specification associated to the sequential composition of statements is the demonic composition of their interpretations. The notation for demonic composition is from [START_REF] Frappier | A relational calculus for program construction by parts[END_REF]. For angelic composition, we use a similar notation rather than (;) to prevent confusion with sequential composition of statements.

Iteration. The while statement is interpreted as a least fixpoint (lfp for short) of a function from specifications to specifications. An encoding of the lfp in type theory is given below. It says that a pair (s, s

) ∈ lfp(F ) iff (s, s ) is in all specifications X such that (F X ⊆ X). lfp (F : Spec → Spec) def = λ s s ⇒ ∀ X • (∀ s s • F X s s → X s s ) → X s s Demonic composition is right-monotonic w.r.t. inclusion of specifications. As a consequence, the function (λ X ⇒ ([[S]] X ) C [[skip]]
) is monotonic. Hence, by the Knaster-Tarski fixpoint theorem, its least fixpoint is defined since the binary predicates ordered by implication (i.e. relations ordered by inclusion) form a complete lattice. We have formalized enough fixpoint theory to prove that lfp indeed represents the least fixpoint. An interesting by-product of this least fixpoint definition of the while statement is the existence of the following well-founded relation associated to each while statement:

≺ C P def = λ s s ⇒ C s ∧ [[P ]] s s ∧ (∃ s • [[while C do P done]] s s )
This relation has been used to proceed by well-founded induction in proving many intermediate results and some of the subsequent theorems.

The refinement relation

The refinement relation occupies unsurprisingly a central place in our development. Intuitively, it corresponds to a kind of translation of the classical relational interpretation (as found in e.g. [START_REF] Spivey | The Z notation[END_REF]) in predicative terms.

Definition 2 (Predicative refinement). We say that S 2 refines S 1 if and only if whenever S 1 terminates on some state s, S 2 terminates on s and all observable behaviors of S 2 on s are observable behaviors of S 1 on s:

S 2 S 1 def = ∀ s • (∃ s • [[S 1 ]] s s ) → (∀ s • [[S 2 ]] s s → [[S 1 ]] s s ) ∧ (∃ s • [[S 2 ]] s s )
This definition reflects the fact that reducing non-determinism or enlarging the domain of a statement moves it down the refinement ordering. The correctness of the design rules relies on important properties of the refinement relation, some of which are stated in the following Lemma.

Lemma 1 (Properties of refinement). Let P and Q designate statements, and let C designate a condition. The following properties hold:

1. P P 2. P Q → Q R → P R 3. P 1 Q 1 → P 2 Q 2 → if C then P 1 else P 2 endif if C then Q 1 else Q 2 endif 4. P 1 Q 1 → P 2 Q 2 → P 1 ;P 2 Q 1 ;Q 2 5. P Q → while C do P done while C do Q done
Essentially, this lemma states that the refinement relation is a preorder, and that the control structures of our language are monotonic w.r.t. refinement. Property (2) justifies the design rule for specified blocks, whereas properties ( 3) and ( 4) justify the design rules for the if statement and sequential composition. Note that these properties of refinement need never be explicitly used to discharge proof obligations. Indeed, the properties are seamlessly applied during the composition of program designs. For example, the nesting of specified blocks implicitly invokes the transitivity of refinement. Actually, the composition of program designs feels like programming, but also consists in constructing (behind the scenes) the main frame of the proof of correctness.

The special case of loops

The predicative semantics of loops corresponds to the least fixpoint of a rather complex function. Even though it is possible to prove refinements by applying the least fixpoint axioms directly, it proves to be a rather impractical method. Hence, we need another way to handle the while construct. In particular we would like to be as uniform as possible and rely on the notion of specification only. Note that Lemma 2 below provides an alternative characterization of loops as if statements under some conditions.

Lemma 2 (Loop Summarization).

well founded (λ s s ⇒ C s ∧ [[P ]] s s ∧ C s) → (if C then P endif; if C then P endif) if C then P endif → while C do P done ≡ if C then λ s s ⇒ [[P ]] s s ∧ ¬(C s ) endif
This summarization lemma is inspired by the relational approach described in [START_REF] Frappier | A relational calculus for program construction by parts[END_REF], and suggests the following design method for loops. First, one should start with a loop body satisfying the conditions of Lemma 2. This first step consists in finding an abstract specification of what the loop body is intended to achieve. Then, one applies the summarization lemma and checks that the loop summary refines the desired specification. Finally, the loop body may be further refined with a more precise implementation. In this way, the lfp definition never appears explicitly in refinement statements to prove. This method rests on the following theorem, which builds on the previous Lemma to give necessary and sufficient conditions for a while statement to refine a given specification.

Theorem 2 (Loop refinement rule).

while

C do P done R ↔ ∃ K L • P L ∧ well founded (λ s s ⇒ C s ∧ [[L]] s s ∧ C s) ∧ K = if C then L endif ∧ K;K K ∧ if C then λ s s ⇒ [[L]] s s ∧ ¬(C s ) endif R
Combined with properties (2) and ( 5) of Lemma 1, this theorem justifies the design rule for the while statement. Note that the second hypothesis of Lemma 2 implies that the relation (λ s s ⇒ C s ∧ [[P ]] s s ) is transitive. This means that in general the loop body must have a non deterministic specification for loop summarization to apply. Hence, the ability to specify non deterministic behavior is key even when the end goal is a deterministic program.

Note 1. The most common way of dealing with loops is through the use of invariants and variants. In the case of the square root algorithm presented in section 2, one can prove correctness in Hoare logic using (r 2 ≤ x < h 2 ) as invariant and (h -r) as variant. If we consider that the intention of the programmer is to have the loop body maintain the invariant and decrease the variant, then the corresponding specification is the following:

(r 2 ≤ x < h 2 ∧ r 2 ≤ x < h 2 ) ∧ (h -r > h -r ) x
This specification states that the invariant is true at the beginning of execution as well as at the end of execution, and also that the variant is lower at the end than it was at the beginning. From the invariant and the variant, one can reason to deduce that the objective is to shrink the search interval and make progress by either increasing r or decreasing h. However, the intention to implement this objective is not so well conveyed by the specification of the loop body when it is written under the invariant-variant mindset. Because specifications are more flexible, the programmer has the opportunity to convey his intentions in a more intelligible way as we did in our example of section 2. In that alternative specification of the loop body, one better sees the search interval closing up towards x.

Refinement in a calculus of weakest prespecifications

In this section we turn our attention to the simplification of p.o.s. Consider the typical situation where a specified block S 1 { S 2 } is introduced. As required by the design rules, the p.a. should prompt us to prove the statement ϕ a (S 2 ) S 1 . However, the current definition of the refinement relation is too primitive as a means to compute such p.o.s. This is mostly due to demonic composition, i.e. the operator. For example, the statement P 1 ;...;P n Q 1 ;...;Q n yields, after unfolding the and operators, a formula containing a profusion of existential quantifiers, and whose size is exponential in n. To avoid such a situation and simplify p.o.s, we recast the definition of the refinement relation in a calculus akin to the classical wp-calculus.

We begin by observing that in Definition 2 the right hand side (r.h.s.) of the implication is (κ([[S 2 ]], [[S 1 ]]) s s), where κ is a relational operator called the conjugate kernel in [START_REF] Desharnais | A relational division operator: the conjugate kernel[END_REF] and the the weakest prespecification in [START_REF] Josephs | An introduction to the theory of specification and refinement[END_REF][START_REF] Hoare | The weakest prespecification[END_REF]. We now translate this operator in a predicative form.

Definition 3 (The weakest prespecification). Let R 1 and R 2 be two specifications. The weakest prespecification of R 2 w.r.t. R 1 is defined as follows:

κ(R 2 , R 1 ) def = λ s s ⇒ (∀ s • R 2 s s → R 1 s s ) ∧ (∃ s • R 2 s s ) Consider K = κ(R 2 , R 1 ) R 2 .
Then the output state s of κ(R 2 , R 1 ) on some input state s is such that R 2 terminates on s , and whatever R 2 does to s , the overall resulting behavior of K is a behavior of R 1 . Specializing κ to the statements of our language and simplifying the resulting expressions, leads to the following specification transformer.

Definition 4 (The wpr transformer). We define, by induction on the syntax, the function wpr of type Statement → Spec → Spec as follows:

           wpr(effect f, R) def = λ s s ⇒ R s (f s ) wpr(S 1 ;S 2 , R) def = wpr(S 1 , wpr(S 2 , R)) wpr(if C then S 1 else S 2 endif, R) def = (wpr(S 1 , R) -1 C wpr(S 2 , R) -1 ) -1 wpr(while C do S done, R) def = lfp λ X ⇒ (wpr(S, X ) -1 C R -1 ) -1 wpr(S 1 { S 2 }, R) def = wpr(S 2 , R) wpr( R 2 , R 1 ) def = κ(R 2 , R 1 )
where R -1 def = λ s s ⇒ R s s

In fact wpr(S, R) is equivalent to κ([[S]], R). Also, wpr is monotonic in its second argument, therefore the least fixpoint in the definition of wpr for the while statement is defined. The wpr transformer is encoded as a Coq fixpoint definition by pattern matching on the first argument. The following theorem shows that refinement can be defined in terms of wpr. The definition is a translation of the relational definition in terms of κ from [START_REF] Desharnais | A relational division operator: the conjugate kernel[END_REF].

Theorem 3. ∀ S 1 S 2 • S 2 S 1 ↔ ∀s • (∃s • [[S 1 ]] s s ) → wpr(S 2 , [[S 1 ]]) s s
By using this wpr-based definition of refinement, we get simpler p.o.s for the same reasons that wp computes simpler p.o.s. In some way we have dealt with the operator on the l.h.s. of (i.e. S 2 in Theorem 3). Indeed, wpr(P 1 ;P 2 ;...;P n , R) simplifies to a formula whose size is linear in n after unfolding definitions, and wpr(effect f, R) simplifies to a formula with no additional quantifiers. Remains the r.h.s. of to consider (i.e. [[S 1 ]] in Theorem 3). We observe that:

[[(effect f );R]] ≡ λ s s ⇒ R (f s) s [[(if C then S 1 else S 2 endif);R]] ≡ [[S 1 ;R]] C [[S 2 ;R]] [[(S 1 ;S 2 );R]] ≡ [[S 1 ;(S 2 ;R)]]
By recursively applying the equations above, [[S 1 ]] may in some cases simplify to a formula with no additional quantifiers. In our development these simplifications are done automatically each time a p.o. is computed. Of course the size of p.o.s may still become unmanageable. But, by refining in small steps, one also keeps the size of p.o.s in check. It is the case that the wpr transformer is not of much help when loops are involved, but thanks to Theorem 3 we can fall back on Theorem 2 to avoid the difficulties related to using directly the least fixpoint definition.

Note 2. One might wonder whether it would be possible to achieve the simplification of p.o.s by using the wp-calculus. Indeed this is possible, based on the following connection between wpr and wp from [START_REF] Josephs | An introduction to the theory of specification and refinement[END_REF]: ∀ s•wpr(S, R) s s ↔ wp(S, (R s)) s.

However wpr is a more natural concept in some cases. For example consider the situation where we must refine R . If we know that Q is a step towards a solution, we can compute a candidate P = wpr(Q, R) so that K = P ;Q is a potential solution. Then, if indeed K R we hopefully have a smaller problem to think about (namely finding an implementation for P ). If unfortunately K is not a solution then the problem cannot be solved in this way. This kind of reasoning is not so natural to achieve with the concept of wp since the latter computes a condition (as the name suggests), whereas the decomposition of R into P ;Q requires P to be a specification.

Related work

In this section we put our research work in the context of mainly three areas: the notion of program design, the use of predicative and relational semantics and the more specific comparison with related Coq developments.

On program designs.

A similar notion of program development is proposed in [START_REF] Morgan | The refinement calculus, and literate development[END_REF] to capture the refinement history. A development is defined as a "multiway branching tree" of refinement steps. In this language each specification statement is given an identifier, and refinement steps reference the specifications they refine by these identifiers. This is very much in the line of literate programming [START_REF] Knuth | Literate programming[END_REF] with the important difference that formal specifications replace informal ones. Comparatively, our program designs are based on the notion of specified blocks introduced in [START_REF] Hehner | Specified blocks[END_REF]. Since specified blocks can be nested they naturally represent a tree of design decisions without the need for explicit identifiers: the abstract syntax tree provides enough structure to capture the relevant information. This also means that unlike in [START_REF] Morgan | The refinement calculus, and literate development[END_REF] we have no need to structure a specific database of program and specification fragments.

On the predicative and relational approaches. The semantics of our language of program designs is close to the predicative interpretation of programming constructs of [START_REF] Hehner | Predicative programming part I[END_REF][START_REF] Hehner | Specified blocks[END_REF][START_REF] Hehner | A practical theory of programming[END_REF], with important differences. Firstly, we follow [START_REF] Sekerinski | A calculus for predicative programming[END_REF] by using demonic composition to represent sequential composition, and by equating non termination, termination in an error state, and relational undefinedness instead of using a time variable or a fictitious program state to distinguish between terminating and non-terminating behaviors as in [START_REF] Hehner | Predicative programming part I[END_REF][START_REF] Hoare | Unifying theories of programming[END_REF][START_REF] Spivey | The Z notation[END_REF]. Representing non termination by undefinedness means however that we cannot for example, specify a program choosing nondeterministically to either terminate or loop forever on a given input. The second difference has to do with our refinement proof rule for loops which is more in the line of [START_REF] Frappier | A relational calculus for program construction by parts[END_REF] where the focus is on assigning abstract specifications to loop bodies rather than on attaching outer specifications to loops as in [START_REF] Hehner | Specified blocks[END_REF]. A loop proof rule similar to ours follows from the results presented in [START_REF] Frappier | A relational calculus for program construction by parts[END_REF], but our rule has weaker requirements and is provably complete.

On refinement in the Coq proof assistant. There are other works of mechanization of refinement theories in the Coq p.a., in particular [START_REF] Boulmé | Intuitionistic refinement calculus[END_REF] and [START_REF] Alpuim | Embedding the refinement calculus in coq[END_REF], both based on the refinement calculus [START_REF] Morgan | The refinement calculus[END_REF]. The goal of the development presented in [START_REF] Alpuim | Embedding the refinement calculus in coq[END_REF] is to derive imperative programs by applying validated refinement rules in proof mode. As a consequence the final program design entangles the intermediate refinement steps together with their proof of correctness. The mechanization of the refinement calculus presented in [START_REF] Boulmé | Intuitionistic refinement calculus[END_REF] supports a quite expressive language (with pattern matching and structural recursion), however the language does not include features to structure the refinement steps. Our work also differs with existing approaches in the way we treat loops. In [START_REF] Alpuim | Embedding the refinement calculus in coq[END_REF] one must specify loop invariants while our formalization allows to specify loop bodies as input-output relations, which is more general. In [START_REF] Boulmé | Intuitionistic refinement calculus[END_REF] one has to work with the fixpoint characterization of loops while we use a more convenient rule. Moreover, we use weakest prespecifications (wpr) instead of weakest preconditions (wp) to compute p.o.s.

Conclusion and future works

We have presented a formalized theory of stepwise refinement. The formalization is the result of our study of both relational and predicative points of view on stepwise refinement, which lead us to a calculus benefiting from some crossfertilization between the two points of view. We have mechanized this formalization thus allowing for correct-by-construction imperative program design in the Coq p.a., even though the scalability of our framework is yet to be improved by extending our language with procedures and a notion of module. One way to take this work further would be to extend this formalization to data refinement [START_REF] Hoare | Proof of correctness of data representations[END_REF], which allows for correct transformation of data representations. One immediate application is then the possibility to refine programs to go from mathematical unbounded data structures (e.g. Peano integers) to bounded data structures (e.g. machine integers), thus permitting a more faithful translation into an actual programming language such as C, Ada or Caml.

Working directly with predicates instead of an embedding of the syntax would greatly simplify matters as this would eliminate a level of indirection. Therefore another way to pursue this work is to allow expressing imperative programs directly with predicates hence fully realizing predicative programming. As this would require manipulating Coq terms directly, we believe it can be done using a tool such as Template Coq [START_REF] Anand | Typed template coq-certified meta-programming in coq[END_REF], or by developing a dedicated plugin.

Table 1 .

 1 The predicative semantics of the design language

calculus of weakest preconditions

https://github.com/bsall/AMToPR-ICFEM-2019

The notation S x 1 ,...,xn is a shorthand for S ∧ x 1 = x1 ∧ • • • ∧ x n = xn .

Prop is the built-in type of logical propositions in the Coq p.a.


Jean-Dominique Polack
email: jean-dominique.polack@sorbonne-universite.fr

Generalized formulation for acoustics

come

Introduction

This manuscript is an attempt to derive a generalized formulation for the wave equation in linear acoustics, including the conservation of energy. It makes use of the conservation of the stress-energy tensor, that is, the covariance of the stress-energy tensor is null in linear acoustics, as first proven by P.M. Morse and K.U. Ingard [START_REF] Morse | Theoretical Acoustics[END_REF]. At stake is a novel approach to sound field computation that naturally accounts for losses, whereas current computational methods do not.

As a matter of fact, the stress-energy tensor and its covariant conservation are the basis of general relativity. The present paper therefore investigates to which extend general relativity has application in linear acoustics. Except for its derivation by Morse and Ingard [START_REF] Morse | Theoretical Acoustics[END_REF], there has been no attempt to apply this formalism to acoustics. The motivation behind this investigation was the search for a natural setting for explaining the curvature of rays above absorbing surfaces experimentally proven by Janowsky and Spandöck in the 30s [START_REF] Janowsky | Aufbau und Untersuchungend eines schallgedämpften Raumes[END_REF], and confirmed by Cremer and Müller [START_REF] Cremer | Die wissenschaftlichen Grundlagen der Raumakustik[END_REF].

The generalized wave equation

We consider a 4-dimensional time-space with its metric tensor g ij and the volume element dV = |g|dx 0 . . . dx 3 , where g = det g ij [Lin 5]. The infinitesimal distance element is given by:

ds 2 = g ij dx i dx j (1)
and the generalized wave equation is:

Φ = i g ij ∂ j Φ = 0 (2)
where Φ is the velocity potential and g ij the inverse matrix of g ij . Note that i is the covariant derivation with respect to x i , which differs from the usual partial derivation ∂ i in a way that depends on the tensor rank. For example, for a function Φ:

j Φ = ∂ j Φ = Φ j 1 but j Φ i = ∂ j Φ i -Γ k ji Φ k and j X i = ∂ j X i + Γ i jk X k
, where X i are the (contravariant) components of vector X and the Γ k ji the Christoffel symbols linked to the derivatives of the elements of the metric tensor g ij :

Γ k ji = 1 2 g kl (∂ j g il + ∂ i g lj -∂ l g ji ) (3)
Note that, unlike ordinary differentiations, covariant derivations do not commute. Their commutators is given by the curvature of the time-space [Lin 5]:

( i j -j i ) X k = R k mij X m (4)
where the R k mij are the elements of the Riemann tensor. However, for a function, i ∂ j Φ = j ∂ i Φ; and by construction, all covariant derivatives of the elements of the metric tensor are null. In other words, the contravariant derivation i is defined by: i = g ij j = j g ij One calls vectors tensors with one upper index, such as X i ; and covectors tensors with one lower index, such as Φ i .

Volume deformation

In general, the velocity potential Φ is a complex function. So one can consider the product Φ * Φ, where Φ * is the complex conjugate of Φ. Differentiation rules lead to:

Φ * Φ = Φ * i g ij ∂ j Φ = i g ij [Φ * ∂ j Φ] -[∂ i Φ * ] g ij ∂ j Φ = 0 (5)
that is, to:

i g ij [Φ * ∂ j Φ] = [∂ i Φ * ] g ij ∂ j Φ (6)
As the right member of the preceding equation is real, separating the real and imaginary parts leads to:

i g ij Φ * ∂ j Φ + Φ∂ j Φ * 2 = ∂ i Φ * g ij ∂ j Φ = 2L (7)
for the real part, where L is the Lagrangian; and for the imaginary part, to:

i g ij Φ * ∂ j Φ -Φ∂ j Φ * 2i = j Φ * ∂ j Φ -Φ∂ j Φ * 2i = 0 (8)
It should be noticed that g ij Φ * ∂j Φ+Φ∂j Φ * 2 can be rewritten as:

g ij Φ * ∂ j Φ + Φ∂ j Φ * 2 = g ij ∂ j 1 2 |Φ| 2 (9)
that is, as the 4-gradient of a real function. As a consequence, g ij Φ * ∂j Φ+Φ∂j Φ * 2 can be assimilated to a 4-velocity -V i . Thus the real part of Eq. (6) simply reduces to:

i V i = -2L (10)
meaning that the Lagrangian L amounts to a volume deformation (divergence of a velocity). In a similar fashion, the imaginary part

Φ * ∂j Φ-Φ∂j Φ * 2i
can be assimilated to a "covector" potential A j with the gauge relation:

i A i = 0 (11) 2
4 Conservation of the stress-energy tensor

We now consider the product ∂ k Φ * Φ. Once more, differentiation rules lead to:

∂ k Φ * Φ = ∂ k Φ * i g ij ∂ j Φ = i g ij [∂ k Φ * ∂ j Φ] -[ i ∂ k Φ * ] g ij ∂ j Φ = i g ij [∂ k Φ * ∂ j Φ] -[ k ∂ i Φ * ] g ij ∂ j Φ = j [∂ k Φ * ∂ j Φ] -[ k ∂ i Φ * ] g ij ∂ j Φ = 0
As i and j are mute indices, separating the real and imaginary parts of the preceding equation leads to:

• for the real part:

j (∂ j Φ * ∂ k Φ + ∂ j Φ∂ k Φ * ) = k ∂ i Φ * g ij ∂ j Φ (12) that is, to: i T ij = 0 ( 13
)
where T ij is the symmetrical stress-energy tensor, defined by:

T ij = ∂ i Φ * ∂ j Φ + ∂ i Φ∂ j Φ * 2 - 1 2 g ij ∂ i Φ * g ij ∂ j Φ (14)
• for the imaginary part:

j (∂ j Φ * ∂ k Φ -∂ j Φ∂ k Φ * ) = [ k ∂ i Φ * ] g ij ∂ j Φ -[ k ∂ i Φ] g ij ∂ j Φ * = -4πij k (15)
The covector j i can be assimilated to a 4-current, as will become evident in next Section.

It is easy to recognise that the equation for the real part corresponds to the contravariant conservation of the stress-energy tensor, suggesting that T ij be proportional to the Ricci curvature tensor R ij , and its reduction T to the scalar curvature R, linked to the volume variation. This confirms the conclusion from Sec. 3 that T measures a volume deformation.

Maxwell equations

In acoustics, the different coefficients of the stress-energy tensor can be interpreted as [MI68]:

• the total energy density T 00 ;

• the active acoustic intensity

T a0 , a ∈ [1, 2, 3], or T 0a , a ∈ [1, 2, 3]; • the symmetrical wave-stress tensor T ab , (a, b) ∈ [1, 2, 3];
Conservation of the stress-energy tensor T ij therefore amounts to the conservation of energy.

On the other hand, let us introduce the antisymmetric tensor F ij defined by:

F ij = i A j -j A i = -F ji (16)
In other words, F ij is the the external differential form (curl) of the covector potential A. Simple derivations lead to:

i A j = i Φ * ∂ j Φ -Φ∂ j Φ * 2i = 1 2i {∂ i Φ * ∂ j Φ + Φ * i ∂ j Φ -∂ i Φ∂ j Φ * -Φ i ∂ j Φ * } (17) j A i = 1 2i {-∂ j Φ∂ i Φ * + Φ * j ∂ i Φ + ∂ j Φ * ∂ i Φ -Φ j ∂ i Φ * } (18)
and by subtracting the two equations, to:

F ij = i A j -j A i = ∂ i Φ * ∂ j Φ -∂ j Φ * ∂ i Φ 2i (19)
Due to its definition, F ij naturally satisfies the generalized Maxwell equations:

i F ij = -4πj j [k F ij] = k F ij + i F jk + j F ki = 0 ( 20
)
where the square brackets indicate sum over all cyclic permutations, that is, anti-symmetrization. The first equation is nothing else than Eq. ( 15), and leads to assimilate the covector j i to a 4-current. The second equation simply derives from the definition of tensor F ij and the commutative property of covariant derivations. Indeed:

[k F ij] = k [ i A j -j A i ] + i [ j A k -k A j ] + j [ k A i -i A k ] = 0 (21)
Note that the first Eq. (20) implies current conservation. Indeed, form the definition of j i :

j i = i ∂ k Φg kl ∂ l Φ * -i ∂ k Φ * g kl ∂ l Φ 4πi = 1 4π i ∂ k Φg kl ∂ l Φ * (22)
we obtain:

i j i = j g ji i ∂ k Φg kl ∂ l Φ * -i ∂ k Φ * g kl ∂ l Φ 4πi = 1 4πi j g ji i ∂ k Φg kl ∂ l Φ * + i ∂ k Φg kl g ij j ∂ l Φ * - 1 4πi j g ji i ∂ k Φ * g kl ∂ l Φ + i ∂ k Φ * g kl g ij j ∂ l Φ = 1 4πi j g ji i ∂ k Φg kl ∂ l Φ * -j g ji i ∂ k Φ * g kl ∂ l Φ = 1 4πi j g ji k ∂ i Φg kl ∂ l Φ * -j g ji k ∂ i Φ * g kl ∂ l Φ (23)
The commutation relations for covariant derivatives leads to:

j k g ji ∂ i Φ = k j g ji ∂ i Φ + R j mjk g mi ∂ i Φ (24)
We recognize in the first term on the right hand side the generalized wave equation j g ji ∂ i Φ = 0, and the term is therefore equal to 0. Thus:

j g ji k ∂ i Φg kl ∂ l Φ * = R j mjk g mi ∂ i Φg kl ∂ l Φ * = R mk g mi ∂ i Φg kl ∂ l Φ *
where R ik = R j ijk is the Ricci tensor. In a similar fashion:

j g ji k ∂ i Φ * g kl ∂ l Φ = R mk g mi ∂ i Φ * g kl ∂ l Φ
and Eq. (23) becomes:

i j i = 1 4πi R mk g mi ∂ i Φg kl ∂ l Φ * -R mk g mi ∂ i Φ * g kl ∂ l Φ
Since all indices are mute and the Ricci tensor is symmetric, the two terms cancel out. Thus:

i j i = 0 (25)
There remains to interpret the antisymmetric tensor F ij in acoustical terms. By comparison with the stress-energy tensor, it is obvious that F a0 = -F 0a , a ∈ [1, 2, 3] is the reactive acoustic intensity. Therefore, by analogy, we call the terms

F ab = -F ba , (a, b) ∈ [1, 2, 3
] the reactive wave stress.

Solving the generalized wave equation

Let us now consider a 4-dimensional manifold V , with border ∂V = S, metric tensor g ij and volume element dV = |g|dx 0 . . . dx 3 . We consider boundary conditions of admittance type on S:

∂ i Φβ i = 0 ( 26
)
where β i = ξ -iσ i is the complex specific 4-admittance. Solving the wave equation in V with boundary condition (26) on S amounts to finding the extremum of the Lagrangian, that is, the extremum of the volume integral T = V T dV of the volume deformation 2L given by Eq. (10). Using Eq. ( 7), we thus obtain:

2L = 2 V LdV = 1 2 V i g ij [Φ * ∂ j Φ + Φ∂ j Φ * ] |g|dx 0 . . . dx n (27) Using the identity i X i = 1 √ |g| ∂ i ( |g|X i ) [Lin 5
] and applying Stokes theorem, the last expression leads to:

2 V LdV = 1 2 S [Φ * ∂ j Φ + Φ∂ j Φ * ] g ji n i dS (28)
Choosing the local coordinates on the boundary so that n i is the outgoing 4vector, and that g ji n i = ξ j leads to:

[Φ * ∂ j Φ + ∂ j Φ * Φ] g ji n i = [Φ * ∂ j Φ + ∂ j Φ * Φ] ξ j = Φ * ∂ j Φβ j + ∂ j Φ * β * j Φ + iσ j Φ * ∂ j Φ -iσ ∂ j Φ * Φ = 0 + iσ j [Φ * ∂ j Φ -∂ j Φ * Φ] = 2σ j [Φ * ∂ j Φ] (29)
Thus:

2L = 2 V T dV = S σ j [Φ * ∂ j Φ] dS (30)
In a similar way, for the imaginary part, Eq. ( 8) implies:

0 = V j [Φ * ∂ j Φ -Φ∂ j Φ * ] dV = S [Φ * ∂ j Φ -Φ∂ j Φ * ] g ji n i dS (31)
with:

[Φ * ∂ j Φ -∂ j Φ * Φ] g ji n i = [Φ * ∂ j Φ -∂ j Φ * Φ] ξ j = Φ * ∂ j Φβ j -∂ j Φ * β * j Φ + iσ j Φ * ∂ j Φ + iσ ∂ j Φ * Φ = 0 + iσ j [Φ * ∂ j Φ + ∂ j Φ * Φ] = 2iσ j [Φ * ∂ j Φ] (32)
We finally obtain:

S σ j [Φ * ∂ j Φ] dS = 0 ( 33
)
It should be noted that the metric tensor g ij is normalized by |g| = c 2 , but its elements are not bounded. Similarly, the β i are not bounded.

Discussion

The striking aspect of these generalized equations is the presence of Maxwell equations equations to describe the evolution of the reactive intensity and wave stress. They are obtained as the external differential form of a covector potential A i that naturally satisfies the gauge relation i A i = 0. There exist other attempts in the literature to associates Maxwell equations to the energy-stress tensor. Most notable is the Kaluza-Klein theory [START_REF]Kaluza-klein theory[END_REF], derived in the 1920s, and its successors. Unlike Kaluza-Klein theory, the present approach does not introduce an extra dimension to introduce Maxwell equations; nor is the metric tensor modified by the covector potential A i .

The fact that thecovector potential and the Maxwell equations are associated to the reactive intensity field leads to a straightforward physical interpretation: they are associated to standing waves and the eigenmodes of the manifold. Indeed, its is well known that eigenmodes are characterized by a quadrature relation between pressure and particle velocity, that is, by a vanishing active intensity and a non-vanishing reactive intensity. Thus, compared to the local field described by the stress-energy tensor, the reactive field is the global signature due to the manifold geometry. Global and local field are coupled at the boundaries, as shown by Eq. (30).

Examples

We now give a few examples of metric tensors g ij that satisfy the admittance condition (26) on the boundary, with real specific admittance.

Propagation above constant absorbing plane

The case of sound propagation above a constant absorbing plane x 1 = 0 is addressed first. Boundary condition (26) then reduces to ∂ 0 Φβ 0 + ∂ 1 Φβ 1 = 0, with β 0 β 1 = -ξ, the real specific admittance on the absorbing plane. As the outgoing 4-vector is n i = (0, -1, 0, 0), the local metric must satisfy g j1 n 1 = ξ j , that is, g 10 = g 01 is non-zero. In other words, the metric tensor and its inverse are no longer diagonal, and must be written as:

g ij =     -c b 0 0 b a 0 0 0 0 1 0 0 0 0 1     , g ij =     -a b 0 0 b c 0 0 0 0 1 0 0 0 0 1     (34)
where a, b, and c only depend on the coordinate x 1 and not on the two other space coordinates. The boundary condition is then given ∂ 0 Φb + ∂ 1 Φa = 0, with b a = -ξ, the real specific admittance on the absorbing plane. Normalizing a, b, and c by ac + b 2 = 1, it is then obvious that g = det(g ij ) = -1, a > 0, and b ≤ 0.

Lagrangian: Simple calculation shows that the Lagrangian L is given by:

L = 1 2 -c|Φ 0 | 2 + b(Φ * 0 Φ 1 + Φ 0 Φ * 1 ) + a|Φ 1 | 2 + |Φ 2 | 2 + |Φ 3 | 2 (35)
Christoffel symbols: The Christoffel symbols are all equal to 0, except for:

Γ 0 00 = Γ 1 00 = -Γ 1 01 = 1 2 ba 1 , Γ 0 01 = 1 2 ca 1 Γ 0 10 = -Γ 1 11 = 1 2 ca 1 , Γ 1 10 = - 1 2 ba 1 , Γ 0 11 = -cb 1 + 1 2 bc 1 (36)
Stress-energy tensor: The conservation of the stress-energy tensor takes a simpler form for T ij than for T ij , which still is symmetric. Indeed, Eq (13) can be written as:

g lj i T il = g ik k T il g lj = i T ij = ∂ i T ij + Γ i in T nj + Γ j in T in = 0 (37)
that is ([Lin 5] p.54):

1

|g| ∂ i ( |g|T i j ) + Γ j in T in = 0 (38)
or, after integration on a small 4-dimensional volume V with border ∂V :

∂V n i T i j dS + V Γ j in T in dV = 0 (39)
In the last two equations,

T ij = g ik 1 2 (Φ k Φ * l + Φ * k Φ l )g lj -g ij L is given by:     1 2 | -cΦ 0 + bΦ 1 | 2 + |Φ 1 | 2 + c|Φ 2 | 2 + c|Φ 3 | 2 1 2 {(-cΦ 0 + bΦ 1 )(bΦ * 0 + aΦ * 1 )} -(Φ 0 Φ * 1 ) -b|Φ 2 | 2 -b|Φ 3 | 2 {(-cΦ 0 + bΦ 1 )Φ * 2 } {(-cΦ 0 + bΦ 1 )Φ * 3 } 1 2 {(-cΦ 0 + bΦ 1 )(bΦ * 0 + aΦ * 1 )} -(Φ 0 Φ * 1 ) -b|Φ 2 | 2 -b|Φ 3 | 2 1 2 |Φ 1 | 2 + |bΦ 0 + aΦ 1 | 2 -a|Φ 2 | 2 -a|Φ 3 | 2 {(bΦ 0 + aΦ 1 )Φ * 2 } {(bΦ 0 + aΦ 1 )Φ * 3 } {(-cΦ 0 + bΦ 1 )Φ * 2 } {(bΦ 0 + aΦ 1 )Φ * 2 } 1 2 c|Φ 0 | 2 -2b (Φ 0 Φ * 1 ) -a|Φ 1 | 2 + |Φ 2 | 2 -|Φ 3 | 2 0 {(-cΦ 0 + bΦ 1 )Φ * 3 } {(bΦ 0 + aΦ 1 )Φ * 3 } 0 1 2 c|Φ 0 | 2 -2b (Φ 0 Φ * 1 ) -a|Φ 1 | 2 -|Φ 2 | 2 + |Φ 3 | 2     ∂ 0 T 00 + ∂ 1 T 10 + ∂ 2 T 20 + ∂ 3 T 30 + [2Γ 0 00 + Γ 1 10 ]T 00 + [3Γ 0 01 + Γ 1 11 ]T 10 + Γ 0 11 T 11 = 0 ∂ 0 T 01 + ∂ 1 T 11 + ∂ 2 T 21 + ∂ 3 T 31 + Γ 1 00 T 00 + [Γ 0 00 + 3Γ 1 10 ]T 01 + [Γ 0 01 + 2Γ 1 11 ]T 11 = 0 ∂ 0 T 02 + ∂ 1 T 12 + ∂ 2 T 22 + ∂ 3 T 32 + Γ 0 00 + Γ 1 10 T 02 + Γ 0 01 + Γ 1 11 T 12 = 0 ∂ 0 T 03 + ∂ 1 T 13 + ∂ 2 T 23 + ∂ 3 T 33 + Γ 0 00 + Γ 1 10 T 03 + Γ 0 01 + Γ 1 11 T 13 = 0
that is to:

∂ 0 T 00 + ∂ 1 T 10 + ∂ 2 T 20 + ∂ 3 T 30 + 1 2 ba 1 T 00 + ca 1 T 01 -(cb 1 - 1 2 bc 1 )T 11 = 0 ∂ 0 T 01 + ∂ 1 T 11 + ∂ 2 T 21 + ∂ 3 T 31 + 1 2 ba 1 T 00 -ba 1 T 01 - 1 2 ca 1 T 11 = 0 ∂ 0 T 02 + ∂ 1 T 12 + ∂ 2 T 22 + ∂ 3 T 32 = 0 ∂ 0 T 03 + ∂ 1 T 13 + ∂ 2 T 23 + ∂ 3 T 33 = 0
Ricci and scalar curvature: The Ricci curvature tensor can be computed from the derivative of the Christoffel symbols, by contraction of the Riemann curvature tensor on two indices. One obtains successively:

• the Riemann tensor:

R l kij = ∂ i Γ l jk -∂ j Γ l ik + Γ m jk Γ l im -Γ m ik Γ l jm • the Ricci tensor: R ij = R l ilj • the scalar curvature: R = g ij R ij
Lengthy calculations lead to the expression of the Ricci tensor and the scalar curvature:

R 00 = 1 2 aa 11 , R 01 = R 10 = - 1 2 ba 11 , R 11 = - 1 2 ca 11 , R = -a 11
all the other elements being null. Note that the last equation indicates that there always is volume expansion or contraction. However, the Einstein tensor

G ij = R ij -1 2 g ij
R is identically null, in accordance with the fact that acoustical waves are not subject to gravitation.

Ray equation: Sound rays simply follow the equation dx i g ij dx j = 0. With the notations:

x = dx 1 dx 0 , y = dx 2 dx 0 , z = dx 3 dx 0 it reduces to Monge equation: 2bx + c(x ) 2 + (y ) 2 + (z ) 2 = a
Ray curvature can then be computed form the generalized acceleration equation:

dv i dτ = -Γ i kl v k v l
where τ is the proper time defined by dτ 2 = -ds 2 = -g ij dx i dx j and the v i are defined by: v i = dx i dτ We can then write:

dv i dτ = d dτ dx i dτ = -Γ i kl v k v l = d dτ dx i dx 0 dx 0 dτ = d 2 x i (dx 0 ) 2 dx 0 dτ 2 + dx i dx 0 d 2 x 0 (dτ ) 2 = d 2 x i (dx 0 ) 2 (v 0 ) 2 - dx i dx 0 Γ 0 kl v k v l
Thus:

(x i ) = d 2 x i (dx 0 ) 2 = dx i dx 0 Γ 0 kl -Γ i kl v k v 0 v l v 0 (40)
We then obtain the system:

x = x Γ 0 00 + 2Γ 0 01 x + Γ 0 11 (x ) 2 -Γ 1 00 + 2Γ 1 01 x + Γ 1 11 (x ) 2 = 1 2 ba 1 + 3ba 1 x + 3ca 1 (x ) 2 -(2cb 1 -bc 1 )(x ) 3 (41) y = y Γ 0 00 + 2Γ 0 01 x + Γ 0 11 (x ) 2 = 1 2 ba 1 + 2ca 1 x + -(2cb 1 -bc 1 )(x ) 2 y (42) z = z Γ 0 00 + 2Γ 0 01 x + Γ 0 11 (x ) 2 = 1 2 ba 1 + 2ca 1 x + -(2cb 1 -bc 1 )(x ) 2 z (43)
Since a must increase away from the boundary and b is negative, ba 1 is negative and a ray parallel to the absorbing plane (x = 0) is curved down toward the plane, as experimentally observed by Janowsky and Spandöck [START_REF] Janowsky | Aufbau und Untersuchungend eines schallgedämpften Raumes[END_REF]. On the other hand, rays with normal incidence (y = z = 0) are not deviated and remain normal to the surface.

that is:

∂ 0 T 00 + ∂ 1 T 10 + ∂ 2 T 20 + ∂ 3 T 30 + 1 2 ba 1 T 00 + ca 1 T 01 -(cb 1 - 1 2 bc 1 )T 11 +(ca 2 + bb 2 )T 02 + (ca 3 + bb 3 )T 03 + (bc 2 -cb 2 )T 12 + (bc 3 -cb 3 )T 13 = 0 ∂ 0 T 01 + ∂ 1 T 11 + ∂ 2 T 21 + ∂ 3 T 31 + 1 2 ba 1 T 00 -ba 1 T 01 - 1 2 ca 1 T 11 +(ab 2 -ba 2 )T 02 + (ab 3 -ba 3 )T 03 + (bb 2 + ac 2 )T 12 + (bb 3 + ac 3 )T 13 = 0 ∂ 0 T 02 + ∂ 1 T 12 + ∂ 2 T 22 + ∂ 3 T 32 + 1 2 a 2 T 00 -b 2 T 01 - 1 2 c 2 T 11 = 0 ∂ 0 T 03 + ∂ 1 T 13 + ∂ 2 T 23 + ∂ 3 T 33 + 1 2 a 3 T 00 -b 3 T 01 - 1 2 c 3 T 11 = 0

Conclusion

Besides deriving the wave equation and the corresponding energy conservation in generalized coordinates, the present paper has proved the possibility to construct metric tensors g ij that satisfy the boundary condition g ji n i = β i , with β i real, on the border S. However, the initial hypothesis that an analogue to Einstein equation holds in acoustics cannot be maintained. Even though the corresponding Ricci curvature tensor R ij satisfies the relation

i R ij - 1 2 g ij R = 0
with R the scalar curvature, the stress-energy tensor T ij cannot be proportional to the Einstein tensor G ij = R ij -1 2 g ij R, as the metric tensor must be time invariant, and is in fact null in the present applications, as acoustical waves are not subject to gravitation. On the other hand, the stress-energy tensor is decaying with time and cannot be null. The solution of the generalized wave equation must therefore be numerically computed.

Beyond the falsification of the initial hypothesis, some new results have been obtained. Firstly, a generalized equation for energy conservation has been derived, that can now be numerically solved along the line of our previous papers [START_REF] Dujourdy | An energetic wave equation for modelling diffuse sound fields -application to corridors[END_REF][START_REF] Dujourdy | An energetic wave equation for modelling diffuse sound fields -application to open offices[END_REF]. Secondly, the thickness of "adaptation layer" between the surface admittance and the free space above is a free parameter in the theory; it can thus be adjusted to the case at hand, for example to a quarter wavelength as usually hypothesized in room acoustics. Thirdly, ray curvature above finite impedance surfaces has been proved, and a proper explanation to the experimental finding of Janowsky and Spandöck [START_REF] Janowsky | Aufbau und Untersuchungend eines schallgedämpften Raumes[END_REF] can now be given, or to the computational artifice, amounting to multiple reflections of the rays on the boundaries, currently used in Boudary Element Methods (BEM) to compute propagation above flat lossy boundaries of varying admittance [START_REF] Rasmussen | Propagation of road traffic noise over level terrain[END_REF]. Such results provide a validity check of the present generalized formulation for acoustics.

But totally unexpected is the discovery that reactive intensity and reactive wave stress satisfy Maxwell equations. It makes it possible to define some sort of "second order" stress-energy tensor that describes the conservation of the standing waves within the manifold where the acoustic field takes place. This discovery certainly deserves further investigation.

Propagation above plane with varying absorption

We still consider the plane x 1 = 0 with the same boundary condition as in the previous case: ∂ 0 Φβ 0 + ∂ 1 Φβ 1 = 0, with β 0 β 1 = -ξ, the real specific admittance on the absorbing plane. The metric tensor and its inverse are still given by Eq. (34):

with ac + b 2 = 1, a > 0, and b ≤ 0. But now, a, b, and c only depend on the 3 space coordinates x 1 , x 2 , and x 3 .

Lagrangian: The Lagrangian L is not changed:

Christoffel symbols: New non-zero Christoffel symbols must now be considered, besides the ones given by Eq. ( 36):

Stress-energy tensor: The conservation of the stress-energy tensor T ij now becomes: