F Schoefs

E Bastidas-Arteaga

T V Tran

G Villain

X Derobert

Characterization of Random Fields From NDT Measurements: a Two Stages Procedure

Keywords: non-destructive testing, spatial variability, characterization, optimization, inspection, random field

Characterization of randomness and spatial variability of material properties, loading or deterioration processes of structures, from inspection, is a very challenging task that concentrates the improvement of Non Destructive Testing (NDT) tools on more efficient and higher structural coverage. In case of characterization of random loading or material properties, this challenge is arduous because of the limited number of measures and the quasi-infinite potential positions of local failures. This paper presents a two stages procedure for the stochastic characterization of random fields from NDT measurements. According to the stationarity property, the optimal quantity of NDT measurements and their position can be assessed once a quality requirement is included. The proposed procedure allows: (i) to quantify the properties of the ergodic stationary field, and (ii) to assess the second order parameters of the studied random variables. The paper ends illustrating the methodology with an application that considers the inspection of a concrete beam with a capacitive technique. The results indicate that the proposed methodology is useful to identify the parameters of a random field by reducing the number of NDT measures under given quality requirements.

INTRODUCTION 1.Background

Many countries worldwide are increasing expenditures for maintaining existing infrastructure. Within the framework of Bridge Management Systems (BMS), methods based on visual inspection have been firstly developed with a real potential and several applications [START_REF] Estes | Updating Bridge Reliability Based on Bridge Management Systems Visual Inspection Results[END_REF] and new methods and techniques based on measuring and monitoring are still under development [START_REF] Okasha | Integration of structural health monitoring in a system performance based life-cycle bridge management framework[END_REF][START_REF] Sheils | Development of a two stage inspection process for the assessment of deteriorating infrastructure[END_REF][START_REF] Bastidas-Arteaga | Stochastic improvement of inspection and maintenance of corroding reinforced concrete structures placed in unsaturated environments[END_REF][START_REF] Orcesi | Optimization of bridge maintenance strategies based on multiple limit states and monitoring[END_REF]. The extension of these methodologies and the development of new methods for optimizing the management of other assets different than bridges are still under consideration: sewer or railway networks [START_REF] Breysse | Management Strategies and Improvement of Performances of Sewer Networks[END_REF][START_REF] Rhayma | A probabilistic approach for estimating the behavior of railway tracks[END_REF], dams [START_REF] Peyras | Probability-based assessment of dam safety using combined risk analysis and reliability methods -application to hazards studies[END_REF] and wharfs [START_REF] Schoefs | The ad method for modeling expert Judgment and combination of NDT tools in RBI context : application to Marine Structures. Structure and Infrastructure Engineering: Maintenance, Management, Life-Cycle Design and Performance (NSIE), Special Issue[END_REF][START_REF] Boéro | Time-function reliability of harbour infrastructures from stochastic modelling of corrosion[END_REF][START_REF] Bastidas-Arteaga | Sustainable Maintenance and Repair of RC Coastal Structures[END_REF][START_REF] Bastidas-Arteaga | Economic Assessment of Climate Adaptation Strategies for Existing RC Structures Subjected to Chloride-Induced Corrosion[END_REF]. The common challenge is to optimize the allocation of resources for inspection, maintenance and repair from a risk analysis by ensuring an allowable risk [START_REF] Adey | Risk-based approach to the determination of optimal interventions for bridges affected by mutiple hazards[END_REF][START_REF] Rouhan | Probabilistic modeling of inspection results for offshore structures[END_REF][START_REF] Sørensen | Codified Risk-Based Inspection Planning[END_REF][START_REF] Stewart | Spatial time-dependent reliability analysis of corrosion damage and the timing of first repair for RC structures[END_REF]. Reliability methods offer the theoretical background and tools for safety assessment and Risk Based Inspection (RBI) methods account for uncertainty on measurements.

Optimal asset management requires quantifying the condition of the structure from on-site measured data. In the probabilistic thinking, this question has been addressed by random variable modeling and updating methods that have been widely developed during the three last decades. Random variable updating is very useful for condition assessment and reliability updating when a priori distribution is known and data coming from inspections or monitored systems is collected [START_REF] Orcesi | Optimization of bridge maintenance strategies based on multiple limit states and monitoring[END_REF][START_REF] Schoefs | The ad method for modeling expert Judgment and combination of NDT tools in RBI context : application to Marine Structures. Structure and Infrastructure Engineering: Maintenance, Management, Life-Cycle Design and Performance (NSIE), Special Issue[END_REF][START_REF] Straub | Modelling dependency in inspection performance[END_REF]. Basically, the Bayes theorem and its derivative tools (Bayesian Networks) offer the theoretical framework to deal with this issue. The so-called RBI generalizes these approaches in the case of non-perfect inspections by linking inspection and decisions [START_REF] Bastidas-Arteaga | Stochastic improvement of inspection and maintenance of corroding reinforced concrete structures placed in unsaturated environments[END_REF][START_REF] Faber | Risk Based Inspection: The Framework[END_REF][START_REF] Sheils | Investigation of the effect of the quality of inspection techniques on the optimal inspection interval for structures[END_REF][START_REF] Schoefs | Assessment of spatially dependent ROC curves for inspection of random fields of defects[END_REF]. RBI methods are powerful once there is no important spatial or temporal variability involved into the problem. This implies that the location of the most critical defect, from a reliability point-of-view, is known. In these cases, it can be assumed that the spatial distribution of defects in the neighboring zone does not affect the reliability assessment (robustness). Nevertheless, actual progresses in the development and implementation of new NDT techniques or embedded sensors for new and existing structures need to improve these methodologies within three directions:

-Consideration of spatial variability: it has been shown that spatial variability of real infrastructure cannot be described by random variables. Then, spatial randomness should be considered in several problems. For instance, previous studies [START_REF] Stewart | Spatial time-dependent reliability analysis of corrosion damage and the timing of first repair for RC structures[END_REF][START_REF] Schoefs | Assessment of spatially dependent ROC curves for inspection of random fields of defects[END_REF] have found that inspections should also account for the spatial variability of the measured parameters.

-Robust updating: establishing a prior distribution for a whole set of material properties or model parameters for existing structures conditions the result of posterior distributions obtained after probabilistic updating [START_REF] Beck | Updating Models and Their Uncertainties: Bayesian Statistical Framework[END_REF]. The selection of prior distributions is a very difficult task because it is mainly based on the knowledge of experts and then probabilistic updating must be applied with care. Therefore, further research is required to develop new methods or to improve the existing ones to obtain posterior distributions based on robust updating which is less depending on the uncertainties of prior distributions [START_REF] Tran | Improved Bayesian network configurations for probabilistic identification of degradation mechanisms: application to chloride ingress[END_REF].

-Exploitation of data measured from NDT tools: NDT tools offer new possibilities to collect a huge quantity of data by an operator or a new generation of remotely operating vehicles and robots -e.g. [START_REF] Lu | Mechanical properties estimation of functionally graded materials using surface waves recorded with a laser interferometer[END_REF]. These data could be useful for randomness or spatial variability quantification. However, there are many uncertainties and errors inherent to the measure itself and the assessment of a material property or model parameter from a physical measure (speed wave, resistivity, etc.). New research efforts should be addressed to improve the understanding, controlling, and quantifying these sources of uncertainty and error.

Aims and Scope

Recent studies have focused on random field characterization based on NDT measurements. Nguyen et al [START_REF] Nguyen | Assessing the spatial variability of concrete structures using NDT techniques -Laboratory tests and case study[END_REF][START_REF] Nguyen | Non-destructive evaluation of the spatial variability of reinforced concrete structures[END_REF] combined several NDT techniques, kriging and variograms to assess the spatial variability of concrete at different scales (point, local and global). Gomez-Cardenas et al [START_REF] Gomez-Cardenas | New optimization algorithm for optimal spatial sampling during non-destructive testing of concrete structures[END_REF] proposed an two-step approach to optimize the number and position of ultrasound measures required to localize critical zones. The main objective of this paper is to propose a methodology to find an optimal inspection configuration (number and localization of NDT measures) that minimizes the error of identification of probability distributions for a given quantity of interest (resistance, porosity, water content, etc.) with spatial dependency. This study does not focus on the detection of damage and/or critical zones. The paper focuses on second order random variables and it has been developed on the basis of some basic but realistic assumptions about the inspection characteristics and the random field nature. The proposed flowchart considers a unique stochastic field that can be parameterized by the same parameters (for the distribution and the spatial variability) for several components built with the same material and subjected to the same degradation processes (same environment). For the sake of simplicity of the writing and the illustration, we will consider a one-dimensional spatially distributed field. However, this methodology could be extended to characterize a n-dimensional random field. This methodology is mainly based on a two stages procedure (Figure 1):

-The first stage aims to characterize the spatial correlation of the studied stochastic field -i.e. the parameter of a correlation function.

-The second stage is devoted to get "weakly correlated" data on structural components in view to build a sample of events assumed as independent.

The first part of the paper presents the adopted method for representing spatial variability -i.e., the Karhunen-Loève decomposition (Section 2). Section 3 details the proposed two-stages inspection strategy. The optimization of the number and position of NDT measures is based on a quality criterion that is also presented in Section 3. The paper ends with applications to a numerical and a real study cases to illustrate the potential of the methodology (Sections 4 and 5, respectively).

RANDOM FIELD MODELING OF INSPECTIONS

Usual Approaches for Spatial Variability Modeling

Random field theory is useful for modeling spatial variability of a given quantity (material property, deterioration process, load, etc.). Random fields could take several forms more or less complicated depending on the intrinsic characteristics of the structure (material randomness, construction process, etc.) and/or the interactions with external actions (environmental actions, deterioration processes, etc.). A stationary stochastic process can be used to represent spatial variability when the random field can be considered as homogeneous -i.e. the values of the statistical characteristics of this field do not change with the space). For instance, stationary stochastic processes have been used to model the spatial variability of surface chloride concentration [START_REF] O'connor | Experimental Evaluation of the Scale of Fluctuation for Spatial Variability Modeling of Chloride-Induced Reinforced Concrete Corrosion[END_REF], concrete properties [START_REF] Bazant | Statistical Size Effect in Quasi-brittle Structures: II. Nonlocal Theory[END_REF][START_REF] Bazant | Probabilistic Nonlocal Theory for Quasibrittle Fracture Initiation and Size Effect. I: Theory[END_REF][START_REF] Bazant | Probabilistic Nonlocal Theory for Quasibrittle Fracture Initiation and Size Effect. II: Application[END_REF] or soil properties [START_REF] Srivastava | Spatial Variability Modelling of Geotechnical Parameters and Stability of Highly Weathered Rock Slope[END_REF][START_REF] Nobahar | Effects of soil spatial variability on soil-structure interaction[END_REF][START_REF] Griffiths | Influence of soil strength spatial variability on the stability of an undrained clay slope by finite elements. Slope Stability[END_REF][START_REF] Chenari | New method for estimation of the scale of fluctuation of geotechnical properties in natural deposits[END_REF][START_REF] Jaksa | Experimental evaluation of the scale of fluctuation of a stiff clay[END_REF]. In some cases, when a structure is affected by several phenomena that vary with time (e.g. deterioration) and/or with space (concrete casting in several layers), it is modeled as piecewise stationary stochastic process. This type of stochastic field can represent, for example, the vertical spatial variability of the increase of soil strength with depth or the vertical corrosion of structures located in coastal environments [START_REF] Boéro | Time-function reliability of harbour infrastructures from stochastic modelling of corrosion[END_REF]. Figure 2 plots the mean loss of steel thickness due to corrosion with depth for sheet-piles in marine environment where the corrosion process is governed by several phenomena that depend on the exposure zone E at 10, 25 and 50 years (t10, t25 and t50). It can be observed that there is a characteristic for each considered zone -i.e., E∈[E A , E T , E L , E I , E M , E S ], limited by horizontal dashed lines: from the top to the bottom, Aerial (A), Tide (T), Low level of tide (L), Immersion (I), Mud (M) and Soil (S). In this case, a piecewise stationary stochastic field could be used to have a good representation of the spatial variability of the loss of thickness.

Usual Approaches for Inspection Modeling

During inspection, there are many factors that influence the quality of measurements -e.g, environmental conditions, error in the protocol, error due to material variability, and error induced by the operator [START_REF] Breysse | Accounting for variability and uncertainties in NDT condition assessment of corroded RC structures[END_REF]. These factors could lead, for a given inspection, to under or overestimations of the measured parameter. If the parameter is underestimated, the owner could decide "do nothing" when repair is required. On the contrary, an overestimation generates a "wrong decision" where early repair generates overcharges [START_REF] Bastidas-Arteaga | Stochastic improvement of inspection and maintenance of corroding reinforced concrete structures placed in unsaturated environments[END_REF][START_REF] Rouhan | Probabilistic modeling of inspection results for offshore structures[END_REF][START_REF] Sheils | Investigation of the effect of the quality of inspection techniques on the optimal inspection interval for structures[END_REF]. In this paper we will consider inspection as perfect. It means that (i) there is no bias and (ii) the error is negligible or repetitively tests allow to obtain a good estimate of the real value computed as the average of measurements at a given point and therefore to assume error as negligible.

Main Assumptions for Stochastic Modeling

In order to simplify the presentation of the proposed methodology, we consider the following main assumptions about the nature of both the random field and inspection:

-The stochastic field is considered as second order stationary, statistically homogeneous and the type of marginal distribution is known (e.g., Normal). Then, we focus on the characterization of the second order parameters of the marginal distribution -i.e., mean and standard deviation.

In the following applications we will consider a Gaussian random field.

-A larger number of measurements (more than 100) can be performed. It implies that the structure should have important dimensions or constituted by many components. That is allowed by the future generation of inspection with drones or robots.

-Inspections are regularly spaced for simplicity of the campaign planning. However, different spatial configurations of inspections could also be considered in the optimization problem.

-Inspections are considered as perfect as defined in Section 2.2 and in the literature [START_REF] Schoefs | Assessment of spatially dependent ROC curves for inspection of random fields of defects[END_REF].

Karhunen-Loève Expansion

Given a probability space (Ω, F , P), a stochastic field or process with space or time Z is a collection of Z-valued random variables indexed respectively by a set s "space" or t "time". Let us denote Z(x, θ) the one-dimensional stochastic field where θ represents the randomness and x the spatial coordinate. Z(x,θ i ) is called the i th trajectory of this field and corresponds to a given realization θ i of the field for whatever location x. Z(x 1 , θ) is a random variable that is generated by θ at a given location x = x 1 that is characterized by its marginal distribution. Since we consider here only homogeneous stochastic fields, the marginal distribution of Z(x 1 , θ) is independent on the location. For example, if Z(x, θ) represents the one-dimensional random field of the material strength for various beams built with the same isotropic and heterogeneous material, the proposed procedure aims to characterize the marginal distribution of strength from a series of spaced correlated NDT measurements on each component. In this case a trajectory represents one series of one-dimensional measurements on a given beam. A stochastic field is second order stationary if it follows three main properties:

-the expected value E[Z(x, θ)] does not depend on the location x -i.e., E[Z(x, θ)] = µ Z ;

-the variance V[Z(x, θ)] does not depend on the location x -i.e., V[Z(x, θ)] = σ Z 2 ; and -the spatial covariance COV[Z(x, θ), Z(x', θ)] depends only on the distance (x-x').

Thus, the second order stationary is a property restricted to the two first probabilistic moments. It can be shown that various random fields such as geometries of welds for ships [START_REF] Pasqualini | Measurements and statistical analysis of fillet weld geometrical parameters for probabilistic modelling of the fatigue capacity[END_REF] or the spatial distribution of chloride concentration in reinforced concrete (RC) structures can be represented by stationary stochastic fields [START_REF] Schoefs | Polynomial chaos representation for identification of mechanical characteristics of instrumented structures[END_REF]. Note that if E[Z(x, θ)] is not constant with space, the time-dependent trend of the signal can be subtracted and the stationarity properties could be proved for the field (Z(x,

θ) -E[Z(x, θ)]).
Several approaches can be used to represent a stochastic field Z(x, θ): Karhunen-Loève expansion, approximation by Fourier series, approximation EOLE, variograms, etc. [START_REF] Li | Optimal discretization of random fields[END_REF]. In this paper, we select a Karhunen-Loève expansion to represent the stochastic field of the quantity of interest Z(x, θ) (resistance, porosity, water content, etc.). Karhunen-Loève expansion was selected by taking into account its simplicity of implementation and computational time. This expansion represents a stochastic field as a combination of orthogonal functions on a bounded interval [-a, a]:

Z(x,θ) = µ Z + σ Z λ i ξ i (θ) i=1 n kl ∑ f i (x) (1)
where, µ Z is the mean of the field Z, σ Z is the standard deviation of the statistically homogeneous field Z, n kl is number of terms in the truncated expansion, ξ i (θ) is a set of independent centered Gaussian random variables, and λ i and f i (x) are, respectively, the eigenvalues and eigenfunctions that depend on the type of autocorrelation function (ACF) ρ(Δx). It is possible to analytically determine the eigenvalues λ i and eigenfunctions f i (x) for some autocorrelation functions [START_REF] Ghanem | Stochastic Finite Elements -A Spectral Approach[END_REF]. For example, if we assume that the field is second order stationary and we consider an exponential ACF:

ρ(Δx = x 1 -x 2 )=exp - Δx b ⎛ ⎝ ⎜ ⎜ ⎜ ⎜ ⎜ ⎞ ⎠ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ; 0 < b ( 2
)
where b is the an autocorrelation parameter and Δx ∈ [-a, a]. The following transcendental eθuations can be obtained for the exponential ACF:

1 b -ω tan(ωa) = 0 ω - 1 b tan(ωa) = 0 ⎧ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ⎪ ⎪ ⎪ ⎪ ⎪ (3)
where ω is obtained by solving eq. ( 3). If the solution of the second transcendental equation is noted ω*, the eigenfunctions are:

f i (x) = cos(ω i x) a + sin(2ω i a) / 2ω i for even i sin(ω i * x) a -sin(2ω i * a) / 2ω i * for odd i ⎧ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ (4)
and the corresponding eigenvalues become:

λ i = 2 b 1/ b 2 + ω i 2 (
)

for even i 2 b 1/ b 2 + ω i *2 (
)

for odd i ⎧ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ (5)
The spatial variability of various material properties or model parameters could be represented by an exponential autocorrelation. For instance, Figure 3 presents an autocorrelation function computed from cone penetration tests measurements in Australia [START_REF] Jaksa | Experimental evaluation of the scale of fluctuation of a stiff clay[END_REF]. It is noted that an exponential ACF as the described by eq. ( 2) could be used to represent the spatial autocorrelation of the measurements. The exponential ACF is adopted herein because we found that the experimental autocorrelation of the spatial measures presented in section 5 follows this trend. However, other ACFs could be more appropriate to describe the spatial variability of other parameters.

DESCRIPTION OF THE PROPOSED METHODOLOGY

3.1.

Proposed procedure

This methodology focuses on optimizing identically spaced inspections on structural components of similar characteristics -i.e., built with the same material and exposed to similar conditions. For instance, a set of 1D components (beams), or a large 1D-component subdivided artificially or physically (expansion joint or construction joints as pipe joints in a water network) in a set of short components, or belonging to a wall type structure (steel sheet pile or concrete wall). For illustrating the methodology, we consider a set of large 1D-components (beams). Section 4.4 discusses the case of small components for which characterization of spatial variability is difficult.

By using the results of inspections and random field modeling, we propose a two stages inspection method that provides: (i) the parameters of the spatial autocorrelation function and (ii) weakly correlated measurements that are gathered to build a sample used to characterize the statistics and the marginal distribution of Z. Figure 1 presents the flowchart of the proposed methodology.

The first stage encompasses three starts with an exhaustive inspection with N s1 inspections closely separated at distance L b on a single component. This exhaustive inspection aims at obtaining correlated measurements used to estimate the autocorrelation parameter b (eq. ( 2)). By assuming that the random field is ergodic, one trajectory is sufficient to characterize the whole joint distribution of the stochastic process. L b is mainly defined by expert knowledge. If there is no information about L b , a small distance could be used. It could be reduced if there is no correlated information between two consecutive measures. This stage also requires the definition of the expected precision and confidence of the estimates to characterize. The following two steps are carried out when this information is available:

Step 1.1 -Assessment of the autocorrelation parameter and first estimates of Z: the experimental autocorrelation computed by the procedure described in Section 3.2. Once b is estimated, it is possible to use eq. ( 2) to determine an inspection distance, L c , which provides weakly correlated events for Z during the inspection of the components. L b and L c can be related by the generic term IDT for Inspection Distance Threshold. Thus, L b and L c should satisfy:

L b ∈]0, IDT[ and L c ∈ ]IDT, L[
where L is the length of the component. The IDT is defined by assuming that after a given distance, the events measured from an inspection can be considered as weakly correlated. A Spatial Correlation Threshold (SCT) of the spatial autocorrelation is used to determine IDT. Thus from eq. ( 2), the relationship between IDT and SCT is:

IDT = -bln(SCT) (6)
For instance, for b = 20cm and SCT=0.2, IDT=32.2 cm. The selection of a given SCT value will influence the parameter estimate precision. Such an aspect is illustrated in detail in section 4.2.

Besides determining b, the data obtained from the inspection on the first component (weakly correlated measures) is considered to determine first estimates of the mean µ Z and σ Z and the standard deviation of Z.

Step 1.2 -Optimization of the number of measures by using Monte Carlo simulations: the parameters b, µ Z and σ Z are used for modeling inspection trajectories by combining eq. ( 1) and Monte-Carlo simulations. Each simulation simulates an inspection over a new component. Various components (whole structure) are simulated. The distance between two consecutive simulated measures for each trajectory is L c . These simulations are devoted to determine an optimal number of inspections in terms of the precision and confidence on the estimates that are required by the asset owner (Section 3.3). Consequently, depending on the structural constraints (e.g., number and length of components) the outputs of this stage are the minimum: (i) number of components N t , and (ii) number of inspections per component N s separated by a distance L c .

Once Stage 1 provides an optimal configuration for new NDT inspections, Stage 2 focuses on the statistical characterization of µ Z and σ Z as indicated in the following step (Figure 1):

Step 2.1 -Assessment of µ Z and σ Z : New NDT measurements are carried out by considering the configuration provided by stage 1 (N t , N s and L c ). Data estimated from these weakly correlated NDT measurements is finally used to assess the statistical parameters of Z.

Assessment of the Autocorrelation Parameter from Discrete Inspections

We assume that the stationary stochastic field can be characterized by an exponential ACF that depends on a parameter b (eq. ( 2)) and that a trajectory is sufficient to characterize the whole joint distribution. However, the methodology can be applied to other ACF for different applications [START_REF] Li | Optimal discretization of random fields[END_REF][START_REF] Kenshel | Influence of spatial variability on whole life management of reinforced concrete bridges[END_REF].

Let us focus on the assessment of this ACF from experimental data Z (obtained from sensors or NDT tests). Then, the autocorrelation between two observations z 0 and z k , ρ k is given by [START_REF] Chenari | New method for estimation of the scale of fluctuation of geotechnical properties in natural deposits[END_REF]:

ρ k = i=1 n b -k ∑ z i -µ Z ( ) z i+k -µ Z ( ) i=1 n b ∑ z i -µ Z ( ) 2 with 0 ≤ k < n b (7)
where z i is the value of Z at location i, µ Z is the mean value of Z and n b is the number of observations of Z. Two major procedures have been reported in the literature for the estimation of b for a spatially variable property from a database. The first procedure searches b that maximizes the Maximum Likelihood Estimate (MLE) [START_REF] Li | Effect of spatial variability on maintenance and repair decisions for concrete structures[END_REF]. The second procedure, proposed by Vanmarcke [START_REF] Vanmarcke | Random fields: analysis and synthesis[END_REF] and applied in [START_REF] Schoefs | Optimization of inspection and monitoring of structures in case of spatial fields of deterioration/properties[END_REF], estimates the model parameter that provides the best fit to the sample autocorrelation. This last method can lead to a biased estimation when data is lacking. Consequently, we use the MLE for the estimation of b. Thus, the likelihood function writes:

L h = 1 2π exp - ν i 2 2 ⎛ ⎝ ⎜ ⎜ ⎜ ⎜ ⎞ ⎠ ⎟ ⎟ ⎟ ⎟ ⎟ ⎛ ⎝ ⎜ ⎜ ⎜ ⎜ ⎜ ⎞ ⎠ ⎟ ⎟ ⎟ ⎟ ⎟ i=1 k ∏ = 1 2π ⎛ ⎝ ⎜ ⎜ ⎜ ⎜ ⎞ ⎠ ⎟ ⎟ ⎟ ⎟ k exp - ν i 2 i=1 k ∑ 2 ⎛ ⎝ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎞ ⎠ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ (8)
where ν i is the i th component of the vector of independent standard values obtained from:

ν = C -1 Ẑ -µ Ẑ σ Ẑ ⎛ ⎝ ⎜ ⎜ ⎜ ⎜ ⎞ ⎠ ⎟ ⎟ ⎟ ⎟ ⎟ ( 9
)
where Ẑ is the vector of measurements after inspection of the random variable Z and C a lower triangular matrix such that CC T = ρ and ρ the autocorrelation matrix.

Definition of a reliability oriented measure of quality of inspection

When focusing on a practical application, we aim at optimizing the total number of weakly correlated inspections N=N p ×N s ×N t where N p is the number of repetitive tests for reducing the error of inspection, N s is the number of inspected sections and N t the number of trajectories (Figure 4). Here, the error of inspection is not considered (Section 2.3) and by neglecting the N s1 inspections of the first stage, the total number weakly correlated inspections simply becomes N=N s ×N t .

We use simulated data to find the minimum number of inspections that ensure a given quality of the estimates. In this case the quality will be evaluated with respect to the 'theoretical' expectation and standard deviation of the stochastic field Z (µ Z and σ Z ). µ Ẑ and σ Ẑ are respectively the mean and standard deviation of the stochastic field Z estimated from N simulated measurements after inspection and computed by:

µ Ẑ = 1 N i=1 N ∑ ẑi and σ Ẑ = 1 N i=1 N ∑ ẑi -µ Ẑ ( ) 2 (10)
The quality of a result of inspection can be expressed by several concepts. If we consider the error of measurement, risk oriented measures have been developed: PoD, PFA [START_REF] Rouhan | Probabilistic modeling of inspection results for offshore structures[END_REF], PoI [START_REF] Straub | Modelling dependency in inspection performance[END_REF], PGA and PWA [START_REF] Sheils | Development of a two stage inspection process for the assessment of deteriorating infrastructure[END_REF][START_REF] Bastidas-Arteaga | Stochastic improvement of inspection and maintenance of corroding reinforced concrete structures placed in unsaturated environments[END_REF]. Otherwise, and in case of a finite number of measurements and a finite size of the structure (spatial field effect), other measures can be defined based on distribution tails or a confidence interval of the probability of failure [START_REF] Schoefs | Optimization of inspection and monitoring of structures in case of spatial fields of deterioration/properties[END_REF]. We select in this paper a confidence interval of both the mean µ and the standard deviation σ expressed as a percentage ε (precision) of µ and σ, respectively. We combine random field modeling and Monte-Carlo simulations to estimate the bounds of the confidence interval numerically for target probabilities P ti,µ and P ti,σ for both the mean and the standard deviation, respectively. In a real case, these probabilities could be defined by the asset owner depending on the type of application (structural reassessment, reliability study, etc.). These target probabilities are compared with the following probabilities computed from inspection data:

P Ẑ µ = P µ Ẑ ∈ (1-ε µ )µ Z ;(1+ ε µ )µ Z ⎡ ⎣ ⎢ ⎤ ⎦ ⎥ ( ) (11)
P Ẑσ = P σ Ẑ ∈ (1-ε σ )σ Z ;(1+ ε σ )σ Z ⎡ ⎣ ⎢ ⎤ ⎦ ⎥ ( ) (12)
Eqs [START_REF] Bastidas-Arteaga | Sustainable Maintenance and Repair of RC Coastal Structures[END_REF] and [START_REF] Bastidas-Arteaga | Economic Assessment of Climate Adaptation Strategies for Existing RC Structures Subjected to Chloride-Induced Corrosion[END_REF] are very difficult to estimate. Hence, they are numerically estimated herein by considering data generated from random field modeling. If only a statistical error is considered (measures are independent), confidence intervals theory gives analytical estimates of the precision ( ε µ th and ε σ th ) as a function of the number of measurements N:

ε µ th =u 1-α 2 σ Z µ Z N ( 13
)
ε σ th =u 1-α 2 1 2N (14)
where u 1-α/2 =1.96 for P ti,µ = P ti,σ =0.95. In the case of measurements on trajectories with a weak dependency between data, these values will increase. It is also important to note that both precision and confidence depend on the number of measurements and therefore could be limited by the structural configuration -e.g., the maximum N is limited by the structural size or the number of components.

Depending on the final use of the estimates, several precisions ε or confidence levels P ti can be required for the mean and the standard deviation. The optimal number of inspections can differ between these two estimates. For instance, for optimizing the assessment of µ Z :

N opt ,µ = argmin N P ti,µ ≤ P Ẑµ ( ) (15)
A different value N opt,σ could be obtained for optimizing the assessment of σ Z . Then, the optimal number of measurements N opt writes:

N opt = max N opt ,µ ; N opt ,σ ( ) (16)

APPLICATION TO A NUMERICAL EXAMPLE

Problem Description

This example aims to illustrate: (i) the effect of considering correlated measures in the assessment of the mean and standard deviation of the marginal distribution, (ii) the possibilities for the selection of optimal inspection configurations for specific structures, and (iii) the special case of small size structures. We will therefore consider in the first part a structure with a larger size for which L>>b allowing to assess b from a theoretical point of view. The last part of this section highlights some issues about the size of the structures.

We suppose that the random field to inspect is Gaussian, stationary, ergodic, and characterized by: b = 1m, µ Z = 100 and σ Z = 20 and that the length of the structure is L=200 m. This example does not focus on the assessment of the autocorrelation parameter b. Section 5 will present a complete application of the two-stages methodology for a study case including some considerations for the assessment of b. We aim to provide an inspection protocol that ensures: P ti,µ = P ti,σ = 0.95.

Effect of SCT on the Precision of the Estimates

We first analyze the effect of the choice of SCT on the precision of the estimates quantified by ε µ and ε σ (Figure 5). For N s =20 measurements on a large component (N t =1) with length L=200m, the theoretical values computed from eqs. ( 13) and ( 14) are: ε µ th = 9.3% and ε σ th = 33%. These values correspond to the maximum precision estimated from N=20 independent measurements (statistical error only). It is observed that the precision obtained from consecutive measurements is close to the theoretical value when SCT is small. This effect is more pronounced when SCT is lower than 0.3 for both ε µ and ε σ . Therefore, it is noted that a threshold level of autocorrelation could be defined to provide the distance of inspection. In the following, we fix SCT=0.3 to compute IDT and define L c from eq. ( 6).

Selection of Optimal Configurations for Inspection

As described in Section 3.3, for given precisions (for instance ε µ = 5% and ε σ = 20%) and a fixed L c value, it is possible to estimate the required number of measurements N s and N t to ensure P ti,µ = P ti,σ = 0.95 (eqs. ( 11) and ( 12)). By assuming that SCT=0.3, eq. ( 6) provides that IDT=-bln(0.3)≈1.2m. Since L c ∈]IDT,L[, we select L c =1.2m. Figure 6 presents the couple of minimum required values for N s and N t to guarantee these requirements. For both estimates, the number of measures per component decreases when the number of components is larger. Based on a given structural configuration (e.g., limited number or length of components), Figure 6 illustrates how estimating the number of measures per component N s spaced by L c = 1.2 m on N t components. The number of required measures is almost the same for these quality requirements. However, more measurements will be needed if we require a larger precision on the standard deviation.

The optimization can be also expressed in terms of total number or measurements N. Figure 7 gives the minimum total number of required measurements as a function of the number of available components N t , for instance a given number of beams in a bridge. As indicated by eq. ( 10), there are different optimum values for the mean and the standard deviation. In this case, the optimal number of measures N opt is driven by the assessment of µ Z and computed from eq. ( 11). Here the optimal number is N opt = 40 for N t = 4 components and N s =10 measures per component separated by L c =1.2m. This inspection configuration requires only a total inspection zone of 12m per component. Depending on structural accessibility, the decision maker could decide to perform more spaced measurements that should improve the quality of the estimates. Different conclusions could be drawn if costs of measurements are included in the analysis. For example, the cost of inspecting an additional component could be higher than the cost of increasing the number of measures per component.

Effect of the Size of the Structure

Previous subsections assume that the components are larger enough to find a set of "weakly correlated" measurements. Let us focus on small structures and the related shortcomings for optimal characterization. We consider the same stochastic field as described in Section 4.1 and we decrease the size of a structure from the original length of 200m until 10m. Figure 8 shows the effect of the size of the structure on the precision of the estimates µ Z and σ Z . These results correspond to N=20 measures on a single component. Therefore, the theoretical precisions agree with the values computed in Section 4.2. When SCT>0.8, there is no a unique trend because in this case the measures are very close and only describe the local shape of the inspected trajectory. For components larger than 50m, 20 measurements can be realized whatever SCT. It is consequently observed that for L>50m both ε µ and ε σ converge similarly to the case where L=200m (Figure 5). It is also noted that for shorter components (L=10 and 25m) the values of ε µ and ε σ cannot be computed because it is not possible to carry out 20 measures. Therefore, the convergence until the theoretical value cannot be reached for shorter components. For shorter components, the precision on the assessment of the estimates µ Z and σ Z could be improved by adding more measurements on additional components N t >1. However, if L<b, it could be very difficult to obtain a good characterization of the spatial variability.

APPLICATION TO A STUDY CASE

Description of the Structure and the NDT Tool

The objective of this example is to characterize the marginal distribution and spatial variability of the water content W, modeled as a second order random variable, for a reinforced concrete beam exposed to natural environmental conditions in Bouguenais (Pays de la Loire, France) by using NDT inspections (Capacitive technique). The inspection was performed on the first of March 2012 with high relative humidity of air (H air =99%) and a low temperature (T=5°C). Figure 9 presents the configuration of the experiment. The proposed methodology is applied to inspections on two horizontal trajectories called Line A and Line B. A vertical distance of 40 cm separates these lines. To neglect the error of the measurement, we performed N p =30 repetitive tests on each point and we select the mean value to represent the reference measurement of water content at each point. Figure 9 also includes the histogram for these N p =30 repetitive tests. Therefore, according to Section 2.2, we justify the assumption that these repetitive tests will provide a "perfect" measurement. The repetitive tests are carried out on N s =80 horizontal points separated by 20 cm for each line.

Figure 10 presents the experimental devices. The principle of the Capacitive technique is based on the resonance frequency measurement of an oscillating circuit (around 30-35 MHz) between several electrodes lying on the upper face of the concrete slab (Figure 9) [START_REF] Dérobert | Use of capacitive and GPR techniques for nondestructive evaluation of cover concrete[END_REF][START_REF] Villain | Durability diagnosis of a concrete structure in a tidal zone by combining NDT methods: Laboratory tests and case study[END_REF]. As the combination of medium and electrodes behave like a capacitor, a variation of the dielectric properties of the medium induces a shift of the resonant frequency. A calibration enables to obtain directly the concrete relative permittivity from the frequency measurements, which is mainly related to the water content and the mixing components [START_REF] Robert | Dielectric permittivity of concrete between 50 MHz and 1 GHz and GPR measurements for building materials evaluation[END_REF][START_REF] Soutsos | Dielectric properties of concrete and their influence on radar testing[END_REF][START_REF] Dérobert | EM characterization of hydraulic concretes in the GPR frequencyband using a quadratic experimental design NDT[END_REF]. The volume investigated depends on the geometry of the electrodes. In this study, we used larger electrodes to investigate a 6-8 cm depth of concrete, volume that is more coherent with ground penetrating radar measurements. For simplicity, we consider, for this concrete, a linear relationship between relative humidity and NDT outputs:

W = 48.4981-(F c -F air ) 31.753 (17)
where F c and F air are frequency values in RC beam and in the air at situ, respectively. Ongoing studies in several laboratories worldwide are searching for more accurate relationships by considering a multitechnique approach to account that each NDT tool is sensitive to humidity, porosity, size and type of aggregates.

Data and Modeling

Figure 11 presents the two trajectories obtained for lines A and B based on measures with a filter that remove the few outliers. The shape and the values are different for each line. Line A shows more variability but lower values in comparison to line B. It is expected to find lower water content in the line A because the drying process is faster in the upper zones -i.e., they are more exposed to wind and there is a diffusion of water through the lower zones. The variability could also be explained by other factors as the segregation of concrete. Taking into account this variability with height, we cannot merge the data of both lines to estimate the marginal distribution of W in this practical application. Therefore, in this case we will use the data from one trajectory to characterize the spatial variability and recommend an optimal number and spatial distribution of measures for the second trajectory. We verify first that the autocorrelation shape is similar.

Figure 12 presents the autocorrelation data for trajectories A and B. We obtained a classical shape where the autocorrelation decreases with distance including negative values [START_REF] Chenari | New method for estimation of the scale of fluctuation of geotechnical properties in natural deposits[END_REF]. After fitting the experimental data with eq. ( 2) according to the method presented in Section 3.2, we found that the exponential autocorrelation functions are very close for the two lines. We obtained: b=0.45m and b=0.51m for lines A and B, respectively. It means that the exponential function could be useful to represent the autocorrelation and therefore for modeling the horizontal spatial variability of the water content in RC beams at different depths. Data of line B seems to be more regular (Figure 11) and its experimental autocorrelation is more close to the exponential function. Therefore, in the following, we will use the data from line B to characterize the spatial variability and recommend an optimal number and spatial distribution of measures for the study of the data of line A. Figure 12 only presents autocorrelation values for 8m to illustrate the decay of the values for the first 2 meters; but these values were estimated by considering the information of the whole beam (16m).

First Stage

According to Section 3, the first stage of the inspection methodology is devoted to the assessment of b on a single trajectory. There is an error on the assessment of b because this parameter is deduced from a limited number of measurements N s1 on a given trajectory. This error is mainly due to the number of measurements N s1 on a trajectory (statistical error) and the choice of L b . Although b could be modeled as a random variable B, we decide to consider it as a deterministic value determined from sufficiently correlated measures. b for line B is b=0.51m. Thus, we validate that the inspection distance L b = 0.2m ensures higher correlation between measured data (Figure 12). By defining a SCT=0.3, we can determine IDT=0.61m from eq. ( 6). Then the distance between two weakly correlated inspections is L c =0.6 m for determining the first estimates of µ Z and σ Z that will be used to model the random field. By using the experimental data obtained from this first stage, Figure 13a plots µ B and σ B as a function of the number of measures in the first trajectory N s1 for 1,000 simulated trajectories. The convergence of µ B through the value of b determined from the 80 measurements is faster and the error is less than 0.05m for N s1 ≥ 45 measures. σ B decreases when N s1 is larger by reducing the uncertainty on the assessment of the parameter b.

Figure 13b presents the mean and the 95% confidence interval of µ B for 1000 simulated trajectories as well as the values of b computed from experimental data, as a function of N s1 . The various experimental points for a given N s1 correspond to different sets of N s1 over the total number of measurements. It can be observed that the scatter is large when N s1 decreases and could even reach 0.9m for N s1 =20. It is also noted that b estimated from experimental data is close to µ B when N s1 >45. These results therefore indicate that the assessment of b requires a minimum number of correlated measures N s1 .

Let us now fix the value N s1 =45 measures and optimize the number and spatial distribution of measurements. By considering the autocorrelation parameter identified during the first stage (b=0.51m) and selecting a SCT=0.3, the distance between two weakly correlated inspections is L c =0.6 m. Due to the length of the beam, practically, the maximum number of measures is max(N s, )= 26. This information is used to estimate the theoretical mean and standard deviation from weakly correlated measures µ W,26 =10.12% σ W,26 =0.67%. Values of µ W,26 , σ W,26 and b will be used to optimize the number and spatial distribution of inspections.

Figure 14 describes the effect of the choice of a confidence level (P ti =95% and 90%) on the precisions ε µ and ε σ . After performing Monte Carlo simulations, we plot the evolution of ε µ and ε σ as a function of the number of measures per trajectory N s . The shape of the curves is consistent with the theoretical eqs. ( 13) and [START_REF] Rouhan | Probabilistic modeling of inspection results for offshore structures[END_REF]. Namely, ε µ and ε σ decrease for larger quantity of available data. For all cases, more inspections are required if the confidence level increases. For example, at a given precision level ε µ =10%, the needed number of inspections N s increases from 9 to 12 if the confidence level increases from 90% to 95%. It is also noted that the maximum precisions are limited by the geometry of the structure in this case. For instance, for a confidence level of 90%, the maximum precisions are ε µ =5.2% and ε σ =20% when N s =26 measures.

For the second stage, we fix the following precision levels (ε µ =10% and ε σ =30%) and the confidence interval (P ti,µ = P ti,σ =95%). Consequently, by using the results presented in Figure 14, we obtain the optimum values: N opt,µ =12 and N opt,σ =20 measures. Finally, by applying eq. ( 15), N opt =20 measures. This information will be used to characterize the marginal distribution of the water content on the line A, modeled as a second order variable.

Second Stage and Validation

By considering the output of the first stage (L c =0.6m, and N opt =20 measures), the estimates of the mean and standard deviation of W for the line A are: µ W,20 =9.46% and σ W,20 =0.86%. To verify if these values are within the confidence interval, we take as a reference the mean and the standard deviation for all the 26 weakly correlated measures: µ W,26 =9.37% and σ W,26 =0.85%. This information is also used to compute the bounds of the confidence interval. Thus, Figures 15 and16 present respectively the evolution of µ W and σ W with N s for virtual (simulation) and real inspections and the quality requirements defined in Section 5.3 (ε µ =10%, ε σ =30%, and P ti =95%). For the assessment of the mean, these results confirm that after N opt,µ =12 measures (found for the line B) the estimates are inside the confidence interval. Similar behavior was found for the standard deviation by confirming the optimal value N opt =20 measures for the assessment of both estimates. We observe similar results for the virtual and the real inspection by confirming that this type of simulation is adapted for representing the spatial variability of the water content.

CONCLUSIONS

This paper proposed an original two stages method for the optimal stochastic characterization of random fields from NDT measures in view to (i) assess the shape parameter of the correlation function, and (ii) deduce the parameters of the marginal distribution for a second order variable. Onedimensional stochastic fields with exponential autocorrelation are selected for illustration. The role of the distance between measurements for the stochastic characterization is highlighted and a probabilistic-oriented measure of quality is defined in terms of confidence intervals of the two first statistical moments. That underlines the key role of SCT, the spatial correlation threshold that allows us to rationally define a "weakly dependence" in terms of quality of assessment of the statistical moments. The methodology relies on (i) the assessment of the autocorrelation function on a first trajectory and the use of this information for the optimization of NTD measurements (stage 1), and (ii) the assessment of the parameters of the marginal distribution on a given set of components by knowing the distance between inspections, the number of measures per component, and the number of components (stage 2). The paper ends with practical applications and suggestions for optimizing the stochastic characterization of the water content in a concrete beam by using a capacitive NDT. We found that the optimized configuration ensures the quality requirements.

Further work in this area will be addressed to: -the application to other NDT techniques, -the consideration of other types of autocorrelation functions, -the updating of the optimized configuration and the value of the autocorrelation parameter after inspection of new components, and -the extension of the methodology for optimizing 2D inspection configurations.

LIST OF FIGURES

Figure 1 . 19 Figure 2 . 20 Figure 3 . 20 Figure 4 . 21 Figure 5 . 21 Figure 6 . 22 Figure 7 . 26 Figure 15 . 27 Figure 16 . 27 First 1 -Step 1 . 2 -Figure 1 .

 119220320421521622726152716271121 Figure 1. Flowchart of the proposed methodology. ............................................................................... 19 Figure 2. Mean value of steel thickness loss in each zone at times 10, 25 and 50 years (adapted from [10]). ............................................................................................................................................... 20 Figure 3. Spatial correlation of cone tip resistance in a clay (adapted from [35]). ................................ 20 Figure 4. Definition of the number of inspections. ................................................................................ 21 Figure 5. Effect of SCT on the precisions ε µ and ε σ . ............................................................................... 21 Figure 6. Number of required N s and N t to ensure P ti,µ = P ti,σ = 0.95 (L c =1.2 m). ................................. 22 Figure 7. Total number of measures as a function of N t to ensure P ti,µ = P ti,σ = 0.95 (L c =1.2m). .......... 22 Figure 8. Effect of the size of the structure on the precisions ε µ and ε σ . ................................................. 23 Figure 9. Configuration of the inspection at the RC beam. .................................................................... 23 Figure 10. Devices used for obtaining the NDT data. ............................................................................ 24 Figure 11. Experimental trajectories of W. ............................................................................................. 25 Figure 12. Auto-correlation data and fitted functions for W. ................................................................. 25 Figure 13. Effect of N s1 on the assessment of µ B and σ B . ........................................................................ 26 Figure 14. Influence of N s on the precisions ε µ and ε σ . ........................................................................... 26 Figure 15. Comparison between modeling and real results in the case of ε µ =10% and P ti,µ =95%. ....... 27 Figure 16. Comparison between modeling and real results in the case of ε σ =30% and P ti,σ = 95%. ...... 27

Figure 2 .

 2 Figure 2. Mean value of steel thickness loss in each zone at times 10, 25 and 50 years (adapted from [10]).

Figure 3 . 6 N s = 8 (

 368 Figure 3. Spatial correlation of cone tip resistance in a clay (adapted from [35]).

Figure 4 .

 4 Figure 4. Definition of the number of inspections.

Figure 5 .Figure 6 .

 56 Figure 5. Effect of SCT on the precisions ε µ and ε σ .

Figure 7 .

 7 Figure 7. Total number of measures as a function of N t to ensure P ti,µ = P ti,σ = 0.95 (L c =1.2m).

Figure 8 .

 8 Figure 8. Effect of the size of the structure on the precisions ε µ and ε σ .

Figure 9 .

 9 Figure 9. Configuration of the inspection at the RC beam.

Figure 10 .

 10 Figure 10. Devices used for obtaining the NDT data.

Figure 11 .Figure 12 .Figure 13 .Figure 14 .

 11121314 Figure 11. Experimental trajectories of W.

Figure 15 .Figure 16 .

 1516 Figure 15. Comparison between modeling and real results in the case of ε µ =10% and P ti,µ =95%.

ACKNOWLEDGEMENTS

The authors would like to thank the French regional project ECND-PdL (Non Destructive Control and Evaluation-Pays de la Loire Region) for supporting this study as well as the ERDF (European Regional Development Fund) for supporting the Duratinet project (Atlantic Area Trans-national Cooperation Program 2007-2013 N° 2008-1/049).

Non-Destructive Testing in Civil Engineering NDTCE'09, Nantes, France: 2009: pp. 177-182.


Julien Cohen

A Correct Refactoring Operation to Rename Global Variables in C Programs

Most integrated development environments are shipped with refactoring tools. However, their refactoring operations are often known to be unreliable. As a consequence, developers have to test their code after applying an automatic refactoring.

In this report, we consider a refactoring operation (renaming of global variables in C), and we prove that its core implementation preserves the set of possible behaviors of transformed programs. That proof of correctness relies on the operational semantics of C provided by Compcert C in Coq. We also prove some static properties of the considered refactoring operation and we use them to find properties of some composed refactoring operations.

Introduction 1.Refactoring tools are unreliable

Problem 1: Refactoring tools are not reliable. Designing refactoring tools is a complex task because of the complexity of the underlying programming languages. As a result, probably all refactoring tool suffer from small bugs, that occur in rare cases, but that make those tools unreliable. Many programmers have faced situations where the refactoring tool changed their program in an unexpected way. Recent work have found tens of bugs in several refactoring tools [START_REF] Mongiovi | Safira: A tool for evaluating behavior preservation[END_REF][START_REF] Soares | Automated behavioral testing of refactoring engines[END_REF] by systematic testing. This situation prevent programmers to trust their tools.

There are some refactoring tools, such as the Haskell Refactorer [START_REF] Li | The haskell refactorer, hare, and its api[END_REF] that are rigorously designed and developed, but they are finally not free of bugs. 1This make refactoring tools unreliable. It regularly occurs that one triggers a refactoring operation, then either finds its program broken and then has to unroll the transformation, or discovers at test time that the transformation has changed the behavior of the program in an unexpected way.

Problem 2: Composition of refactoring operations is hazardous. Basic refactoring operations are sometimes used as building blocks for more complex transformation. For instance, the refactoring tools for Java in IntelliJ IDEA and Eclipse internally use the operation pull-up method to provide the operation extract superclass. Another example is the transformations of modular architecture described in [START_REF] Cohen | Views, Program Transformations, and the Evolutivity Problem in a Functional Language[END_REF] (with the Haskell Refactorer, 19 operations used) and [CDA12, AC13, ACR13] (with IntelliJ Idea, 37 operations were used). In such composed transformations, a fault in any of the basic operation makes the whole chain impracticable.

Moreover, when one wants to build a static analysis on composed operations (as in [START_REF] Kniesel | Static composition of refactorings[END_REF][START_REF] Cohen | Practical use of static composition of refactoring operations[END_REF]), the properties basic refactoring operation cannot be formally verified, which make the whole analysis unsound.

Proving properties of refactoring tool operations

Testing and proving are complementary approaches to software validation. Although the need for safe refactoring tools is recognized [START_REF] Schäfer | Challenge proposal: Verification of refactorings[END_REF][START_REF] Brant | Refactoring tools are trustworthy enough and trust must be earned[END_REF], few efforts have been done in this way. For instance, proofs of correctness of refactoring tools are restricted to small languages, such as [START_REF] Sultana | Mechanical Verification of Refactorings[END_REF]. To the best of our knowledge, no such work exists for industrial languages.

Formalized refactoring in Compcert C. Our goal in this report is to make a step towards a fully formalized refactoring tool for an industrial language. We choose C language because is has a mechanized formalization : Compcert C [START_REF] Blazy | Mechanized semantics for the Clight subset of the C language[END_REF][START_REF]Compcert C web page[END_REF]. We present in section 2 how we use Compcert C to build a refactoring tool, and the limits of the approach. Then we focus on a refactoring operation: renaming global variables. Renaming seems to be inoffensive at first sight, but we will see that there are some pitfalls to be avoided (Sec. 3.1). We show how our implementation handle several situations of masking (Sec. 3.2) and that it preserved the behavior of programs, as expected for refactoring operations (Sec. 3.3.1). We also give some properties of the operation that can be used for static composition (Sec. 3.3.2 and 3.3.3) and we illustrate this with a toy example of composite operation (Sec. 4)

All the properties we give are proved in Coq. The full code and the proofs are available from the author or the project webpage.

Refactoring in Compcert C

The main property we want to prove about refactoring operations is their preservation of the behavior of the transformed program/ To do that we need to have a formal definition of the semantics of programs. We rely on the semantics of C programs formalized in Coq provided by Compcert C, which take into account a subset of ISO C 99 larger than MISRA C 20042 .

That semantics (module Csem in Compcert) is defined on abstract syntax trees (AST), not on source code grammar. For this reason, we focus on AST transformations in this report. This allows to focus on the logic of the transformation, but is also has some limits as described below (Sec. 2.4).

Compcert C syntax and semantics

Abstract Syntax Trees

Identifiers (AST.ident) are represented by integers (BinNums.positive). A map from textual identifier in the original program an integer identifiers is maintained during parsing (intern string defined in the OCaml module Camlcoq).

Programs (AST.program) are represented by the list of their definitions (or declarations) : global variables and functions. A definition is represented by a pair (i, d) where i is the defined identifier and d the content of that definition.

That content is composed of a type and an initialization for a global variable (AST.globdef), and of a return type, a list of parameters, a list of local variables and a body for a function (Csyntax.fundef). Function bodies are represented by statement ASTs (Csyntax.statement). Statement ASTs follow a 13 cases grammar, and rely on ASTs of expressions (Csyntax.expr) that follow a 22 cases grammar.

At leaves, we find in particular the construction Evar (x:ident) (ty:type) to represent local or global variables or function names.

Formal semantics

The semantics for C programs given in Compcert is based on small-step transitions (relation Csem.step). That relation respects the non-determinism of C programs : several transitions can be possible from a given state. Those behaviors embed traces which are lists of observable events, such as outputs, either finite (trace) or infinite (traceinf).

Program Transformations

Our refactoring operations are defined as transformations of syntax trees.

We then use a pretty printer to recover a source file. This is not sufficient for a real-world tool,3 but we focus here on the "provable" part of the transformation.

A program transformation may fail and return an error (Error message) or succeed and return the transformed AST (OK program, see the module Errors of Compcert).

Behavior preservation of Transformations

Traces, external behavior

As expected for refactoring operation, we focus on preservation of external or observable behavior. This boils down to preserve the relation program behaves.

Preservation of that relation ensures preservation of the termination, of the returned result, and of the trace.

We accept that the internal behavior (control flow, memory footprint...) change as many existing refactoring operations imply that. The internal behavior is not reflected in the program behavior type, except for some accesses to global variables.

Because of some insight on the internal behavior (global variables) in traces, we have to preserve traces up to global variables renaming (next section).

Relaxing trace equality

Compcert traces include references to global variables that are not observable if those variables are not volatile (and if libraries do not use them). Since we aim at renaming global variables, we have to accept that traces change up to some renaming.

For this reason, our refactoring operation comes with an operation that describes how traces are modified.

Non-determinism

We do not only want that the possible behaviors of the transformed program are included in the set of possible behaviors of the initial program, we want it to be the same set. For instance, consider the two programs below. You can pass from one to another by applying an extract constant or unfold constant refactoring operation. However, the two programs do not have the same set of possible traces. The first one can only print "AB" whereas the second can print "AB" or "BA". 4 s t r i n g a = "A" ; s t r i n g b = "B" ; i n t main ( ) { i n t r 1 = p r i n t f ( a ) ; i n t r 2 = p r i n t f ( b )

; r e t u r n r 1 + r 2 ; } s t r i n g a = "A" ; s t r i n g b = "B" ; i n t main ( ) { r e t u r n p r i n t f ( a ) + p r i n t f ( b ) ; } This kind of change should be avoided. When this is inherent of the considered refactoring operation, the user should be aware that the behavior is not strictly preserved.

Bisimulation

Bisimulation would require that each reduction/transition step has an equivalent in the two internal behaviors (in the original program and in the transformed program). Bisimulation is not needed. When bisimulation is ensured for a given refactoring operation (such as renaming variables), it can be used to ease the proof of correctness.

Limits of the approach

Working on ASTs implies the following limits :

• (Pre-processing.) We do not take pre-processing into account. We do not reconstruct pre-processor directives.

• (Lexing and pretty-printing.) We do not preserve layout and comments.

• (Bloc variables.) Compcert syntax represents block variables by function local variables in the AST. Since we consider only ASTs, we have no way to considered different maskings in different blocks of functions. In particular, our renaming operation fails to rename x into y on the following program whereas it could be legally transformed (i.e. without capture).

i n t x = 1 ; v o i d main ( v o i d ) { x++ ; { i n t y = 1 ; y++ ; } }
/ * r e n a m i n g x i n t o y i s c o r r e c t h e r e * / Note that this does not affect the correctness of the refactoring operation but it prevents its completeness.

• Some parts of the tool cannot be proven correct in the the same framework and have to be tested.

Refactoring Operation: renaming global variables

We now focus on a refactoring operation that renames global variables. Because of many masking and capture situations, renaming is often considered difficult.5

Specification

Name bindings, masking, captures

The interesting part of renaming variables, of course, is dealing with masking (a local variable masks a global variable when they have the same name). We expect the following features :

• We cannot introduce captures (that would change the behavior).

• We can introduce makings as long as they do not create a capture. For instance, renaming x into y in the program below introduces a new masking, but is correct. i n t x ; i n t f ( i n t y ) { r e t u r n y + 1 ; } / * r e n a m i n g x i n t o y i s c o r r e c t h e r e * / See however the limit explained in Sec. 2.4.

Volatile Variables

We do not rename volatile variables because they are designed to be shared with outside world.

External Functions

The problem. In Compcert C, external function (system calls, library function calls) have a (restricted) access to global variables (see the property extcall properties.ec symbol preserved enforced by the axiom external functions properties in Compcert module Events). This reflects the fact that a global variable can be accessed from a linked library, which source code may not be available. The following program gives such an example: p r i n t f ( "%d\n" , a ) ; } Sufficient Condition. Since we generally cannot propagate the renaming in libraries, we have to assume that the renamed variable is not accessed from external code. 6 This is formalized by the following predicate extcall additional properties (a conjunction of four conditions) where x represents the old name and y the new name (module ExtCall). That predicate is used as a precondition for behavior preservation (Sec. 3.3.1).

Definition does not exhibit var (sem:Events.extcall sem) (x :ident) : Prop := ∀ ge vargs m1 tra vres m2, sem fundef Ctypes.type ge vargs m1 tra vres m2 → ¬appears trace x tra.

Record extcall additional properties (sem:Events.extcall sem) x y : Prop := mk extcall properties {

x not in trace : does not exhibit var sem x ; That predicate is used as a pre-condition on the semantics of external functions and for embedded assembly code (see Fig. 1). It is not set as an axiom because it need only to be ensured for the two names involved in the renaming.

y

Implementation of the transformation

We consider rename x y (when x = y).

Pre-operations. Before calling the transformation defined in Coq we perform these operations (coded in OCaml) :

1. Check that y is not a keyword. This cannot be done in the Coq part because identifiers are represented by numbers in syntax trees.

2. Launch parsing with as few as possible modifications of the AST (the Compcert compiler changes the names of local variables which mask global variables just after parsing but we cannot do the same in order to recover original names in our output).

Top-level checks and transformation. When the AST is available from parsing, the transformation defined in Coq operates as follows (see the module Programs, function rename globvar hard):

1. Check that x and y are different from main.

2. Check that y is not already declared (as a global variable or a function).

3. Check that x is not a function.

4. Check that x is not volatile.

5. Change the declaration of x into of declaration for y.

6. Change occurrences of x in global variable initializations into occurrences of y. Fail is x is used in its own initialization.

7. Propagate the change in functions (see below; can fail).

Renaming in function definitions. • f does not bind x / f does not bind y : Rename x into y in the body of f (a statement). This will report an error if y is encountered.

• f binds x / f binds y : Do not change the body of f (masking).

• f does not bind x / f binds y : If x appears in the body of f , report an error (capture). Else do not change the body of f .

• f binds x / f does not bind y : Do not change the body of f (masking). Also check that y does not occur in the body of f . Otherwise, we would transform an ill-formed program into a well-formed program, as for the following progam : 7 i n t x ; i n t f ( i n t x ) { r e t u r n y ; / * t h i s i n s t a n c e o f y i s f r e e * / } Statements and Expressions. Renaming is propagated to the Evar leaves of AST of Statements and Expressions, returning an error if the new identifier is encountered as a variable name (labels are not checked).

Definition change ident untyped (x : AST.ident) (y:AST.ident) i := if AST.ident eq x i then OK y else if AST.ident eq i y then Error (msg "replacing identifier already occurs") else OK i .

We also report an error in some cases that are avoided by construction (some constructors in the grammar of external calls are introduced only during compilation phases of Compcert C ; this is formalized as a precondition, see RawGlobals.rawglobals in Sec. 3.3.1). • We suppose that external libraries and embedded assembly code does not accesses the renamed variable or do not use the new variable name (hypothesis EXT1 and EXT2 in Fig. 1, see Sec. 3.1.3).

Properties

Behavior preservation

• We assume the AST comes directly from the parser and thus does not contain any optimization of accesses to global variables (hypothesis RG in Fig. 1).

• We consider the transformation succeeds (rename globvar hard x y p = OK t p) and then does not report an error (see Sec. 3.2 and3.3.2 for error cases).

Main Result. Under these conditions, the resulting program has the same behavior up to renaming in the trace. This is formalized by the theorem behavior preserved1 (Fig. 1) proved in Coq (in module Correctness). This theorem means that if the original program can produce a trace, the transformed program can produce the same trace, up to renaming in the trace (see Sec. 2.3.2).

Moreover, we have a symmetric result (theorem behavior preserved2 in module Correctness) that states that if the transformed program can produce a trace, then the original program can produce the same trace (up to renaming). 8Those two results allow to say that the original program and the resulting program have the same set of possible behaviors (non-determinism is preserved).

Structure of the Proof. The key lemma to prove the main result it the preservation of transitions (Fig 2).

Renaming does not change the control flow of the program. For this reason, we can exhibit a bisimulation at each level of semantics (expression reduction, see module Reduction, state transitions, see module Step). To do this, we build a correspondence between states coming from the execution of the initial program with states in the execution of transformed program (function change ident in module State). That correspondence relies on correspondences between continuations, between contexts, and between global environments (defined in modules Continuations, Contexts and GlobalEnv).

Difficulties. Those correspondences on continuations, contexts and global environments are tricky to build for different reasons. For continuations, bindings are not always explicit and have to be analyzed before propagating a renaming (as for function bindings). For contexts, Compcert uses an higher order representation which makes context transformation difficult. For global environments, Compcert uses dependant types which forbid the use of some usual tactics in Coq. These points are explained in App. A.

Another technical difficulty is the large number of cases in grammars (types of expressions, statements and continuations) that make quadratic analyses (injectivity proofs for instance) very heavy in time and memory (some tactics take more than 10 minutes at 2 Ghz and more than 4 GB of memory).

Open questions.

• What can we say about ill-formed programs? We only deal with programs for which parsing is successful. What kind of errors does it reject, what kind of errors does it accept?

• What can we say (and prove) about internal behavior (memory usage for instance)?9

• What are the cases we reject and that would be legally renamed (as explained in Sec. 2.4) ?

Lemma step commut : ∀ x y ge tr ge st1 tr st1 tra tr tra st2 tr st2, The transformation fails (returns an error) in some problematic situations where the behavior would not be preserved. Here we describe the conditions on programs that make the transformation succeed.

Necessary preconditions. The following lemmas gives some necessary preconditions.

Lemma rename not defines globvar : ∀ x y p t p, x =y → rename globvar hard x y p = OK t p → ¬ Bindings.defines globvar prog y p .

That lemma states that the new name must not be bound to a global variable.

Lemma rename not defines func : ∀ x y p t p, x =y → rename globvar hard x y p = OK t p → ¬ Bindings.defines func prog y p .

That lemma states that the new name must not be bound to a function.

Lemma rename appears free : ∀ x y p t p, rename globvar hard x y p = OK t p → ¬ Bindings.appears free y p ∧ ¬ Bindings.appears free x p .

That lemma states that the renaming fails if the new name or the old name appear free in the program.

Lemma rename defines : ∀ x y p t p, rename globvar hard x y p = OK t p → Bindings.defines globvar prog x p.

That lemma states that the old name must be bound to a defined global variable. This points a choice in the design/specification of the renaming operation: one can build a renaming operation that successes if the variable to be renamed does not exist. This choice is not important here.

Sufficient preconditions. We introduce the predicate covers y x f that characterizes situations where renaming x into y in a function f would introduce a capture.

Definition covers y x f := binds y f ∧ ¬binds x f ∧ appears statement x (fn body f ).

The following result shows which conditions are suffient for the ransformation to succeed. The last condition ensures that captures of local variables are avoided whereas other conditions are related to global bindings or good form of programs.

Forward and backward descriptions

We now give some descriptions of the effects of our renaming operation. These descriptions can be used in a static composition calculus. We consider x = y. We also consider z such that z = x and z = y.

The following forward descriptions are proved for rename x y p (and t p refers to the resulting program):

• defines globvar commutes (lemmas defines globvar z, defines globvar x and rename not defines globvar ):

defines

Static Composition

In this section, we illustrate static composition by giving some properties of composed refactoring operations from the properties of their components.

We suppose we want a refactoring operation that switches the names of two variables. We are going to build that operation by using the simple renaming operation as a black box.

A Naive attempt

We first consider the following implementations.

Definition swap0 x y p := do p1 ← rename globvar hard x y p ; rename globvar hard y x p1.

We find that y cannot appear in the resulting program (lemma defines globvar back below), which obviously violates the intuitive specification of the operation.

Lemma defines globvar back : ∀ x y p t p, x = y → swap0 x y p = OK t p → defines globvar y t p → False. Proof. intros x y p t p T. monadInv T. apply rename not defines x in EQ0 ; auto. Qed.

Note that this result is obtained by using only properties given in section 3.3.3. The base component operation is considered as a black box : we do not inspect its code and the analysis is static : we never run the component.

A better Swap operation

We now consider a second implementation : Definition swap x y tmp p := do p1 ← rename globvar hard x tmp p ; do p2 ← rename globvar hard y x p1 ; do p3 <-rename globvar hard tmp y p2 ; OK p3.

The following forward and backward descriptions hold (with x, y, tmp, and z all different). 10

• Forward descriptions (lemmas defines x, defines y, not defines tmp and defines globvar z in module Swap):

→ defines globvar x t p → defines globvar y t p defines globvar tmp p → ⊥ defines globvar z p → defines globvar z t p 10 As for all forward and backward descriptions, the corresponding lemmas consider the transformation has succeeded. One must use these properties in conjunction with preconditions to build the precondition of a composed operation [START_REF] Cohen | Practical use of static composition of refactoring operations[END_REF].

Conclusion

Results

We have built a refactoring tool which logic part is formally described and proved correct. Our tool produces C code that has the same semantics as the initial program. The layout and the preprocessing directives are not preserved in our prototype. Also, separate compilation is not fully supported in our prototype since we do not check the use of the renamed variable in linked libraries.

Related work

• On the formalization of refactoring operations on a core language: [LT05] and [START_REF] Sultana | Mechanical Verification of Refactorings[END_REF] (checked by Isabelle/HOL).

• On automatic testing of refactoring operations [START_REF] Mongiovi | Safira: A tool for evaluating behavior preservation[END_REF][START_REF] Soares | Automated behavioral testing of refactoring engines[END_REF], and automatic testing of refactored programs [MGS + 14, GMH14].

• Using refactoring for formal verification [START_REF] Xiang Yin | Formal verification by reverse synthesis[END_REF] [YKW09], which also needs verified refactoring operations.

Future Work

Validation of widespread refactoring tools. Proving the correctness of refactoring operations made us point some situations that require a deep understanding of C mechanisms. For instance, the fact that any library has a direct access to all global variables of the program (see section 3.1.3) can be unexpected by some programmers. That experience can be used to provide a set a tricky test cases for IDE refactoring tools. As an example, we have found a case that is not well treated in a largely used tool (see footnote 7).

Refactoring ill-formed programs. Some refactoring tools can perform correct refactoring in ill-formed programs, for example when there is a syntax error in a part of the program that is not concerned with a local change. Refactoring such programs is not well covered in our work.

Preserve the layout, preserve the preprocessing directives. Most refactoring tools preserve the layout of programs and our tool could probably adapted with the techniques they use. Preserving pre-processing directives is probably more difficult. This is studied in [Spi03, Vit03, Gar05, Pad09, Spi10].

Separate compilation. Our tool should take into account all the files in the project (other C files, libraries) to be effective. Another possibility is to produce a patch for parts of the project that cannot be inspected or modified, as [START_REF] Henkel | Catchup!: Capturing and replaying refactorings to support api evolution[END_REF] does.

Other refactoring operations. Of course, a large set of popular refactoring operations either atomic or composed are waiting to be verified.

Combine test and proof. Currently, only the AST transformation is proved correct. We use tests to check that the parser and the pretty-printer correctly interact with our AST transformation. We could study which tests are necessary to complement our proof.

A.4 Co-induction for infinite traces

Co-induction can be used to prove some (co-inductive) properties on infinite traces (type Events.traceinf). However, some properties that are usually proved by induction on finite traces/lists cannot be proved by co-induction on infinite traces/lists. This is the case for instance for the negation of other properties, or for equality. That makes proofs on infinite traces more difficult to establish than those on finite traces (see the module TraceInf).

A.5 Global environments as a dependant type

Global environments are implemented in Compcert by structures that embed at the same time plain data (trees) and Coq proofs of properties on those trees (in the style described in [START_REF] Leroy | Programming with dependent types: passing fad or useful tool? Informal minutes of[END_REF]). That makes writing transformations of global environment in Coq more heavy that in the traditional way with separated data structures and properties. In particular, some usual Coq tactics such as rewriting in the goal become unavailable for fundamental reasons.

  The transitive closure of step is used to define the relation program behaves between programs and their possible behaviors. Behaviors are represented with the following data-type [INR15]: Inductive program_behavior: Type := | Terminates: trace -> int -> program_behavior | Diverges: trace -> program_behavior | Reacts: traceinf -> program_behavior | Goes_wrong: trace -> program_behavior.

  / * T h i s i s t h e main program * / v o i d show ( ) ; / * e x t e r n a l f u n c t i o n d e c l a r a t i o n , d e f i n e d i n a l i b r a r y * / i n t a = 0 ; / * g l o b a l v a r i a b l e d e f i n i t i o n * / i n t main ( ) { a = 1 ; show ( ) ; a = 2 ; show ( ) ; } / * L i b r a r y ( s h i p p e d w i t h o u t s o u r c e c o d e ) * / #i n c l u d e < s t d i o . h> e x t e r n i n t a ; / * d e c l a r a t i o n ( n o t a d e f i n i t i o n ) * / v o i d show ( ) {

Figure 1 :

 1 Figure 1: Main correctness result

(Figure 2 :

 2 Figure 2: Commutativity of renaming with transitions (relation step)

Theorem

  sufficient precondition : ∀ x y p, x = y → x = prog main p → y = prog main p → RawGlobals.rawglobals p → defines globvar x p → ¬defines globvar y p → ¬defines volatile globvar x p → ¬defines func x p → ¬defines func y p → ¬appears free y p → ¬appears free x p → (∀ (f : function) (i : ident), List.In (i, Gfun (Csyntax.Internal f )) (prog defs p) → ¬covers y x f ) → ∃ t p, rename globvar hard x y p = OK t p .

  To propagate a renaming in a function f , we first check if f binds x and y by the means of a parameter or a local variable (see propagate change ident below). Statements.change ident x y (fn body f ) ;OK (mkfunction (fn return f ) (fn callconv f ) (fn params f ) (fn vars f ) s).

	Definition force (x :AST.ident) (y:AST.ident) (f :Csyntax.function) :=
	do s ← Definition else OK f
	else force x y f
	.
	Four different situations can occur :

propagate change ident (x :AST.ident) (y:AST.ident) (f :Csyntax.function) := if dec binds x f then if dec binds y f then OK f else if decidable appears statement y (fn body f ) then Error (msg "Replacing identifier occurring in function.") else OK f else if dec binds y f then if decidable appears statement x (fn body f ) then Error (msg "This renaming would introduce an undesired hiding.")

  The following backward descriptions (properties needed on p are deduced from properties desired on t p) are also proved for rename x y p :• defines globvar commutes (lemmas defines globvar z back, rename defines y and rename not defines x ):

	globvar z p → defines globvar z t p
	defines globvar x p → defines globvar y t p
	defines globvar y p → ⊥
	• defines func (lemmas defines func z, defines func x and rename not defines func):
	defines func z p → defines func z t p
	defines func x p → ⊥
	defines func y p → ⊥
	• appears free (lemmas appears free z and rename appears free):
	appears free z p → appears free z t p
	appears free x p → ⊥
	appears free y p → ⊥
	• RawGlobals stable (lemma rg stable):
	raw globals p → raw globals t p
	defines globvar z t p → defines globvar z p
	defines globvar y t p →
	defines globvar x t p → ⊥
	• defines func is stable (lemmas defines func z back, not defines y func, not defines x func):
	defines func z t p → defines func z p
	defines func y t p → ⊥
	defines func x t p → ⊥
	• appears free (lemmas appears free z back, rename appears free2 x and rename appears free2 y):
	appears free z t p → appears free z p
	appears free x t p → ⊥
	appears free y t p → ⊥
	• RawGlobals stable (lemma rg backstable):
	raw globals t p → raw globals p

•

  Backward descriptions (lemmas defines x, defines y (same lemmas as in forward description), not defines tmp back and defines globvar z back in module Swap):

	defines globvar x t p →
	defines globvar y t p →
	defines globvar tmp t p → ⊥
	defines globvar z t p → defines globvar z t p

The author of this report reported several bugs in the Haskell Refactorer (2010,

2011) while preparing the work described in[START_REF] Cohen | Views, Program Transformations, and the Evolutivity Problem in a Functional Language[END_REF].

See http://compcert.inria.fr/compcert-C.html#subset for the list of unsupported features.

Other tools (at least IntelliJ Idea, Eclipse and HaRe for Haskell) transform the AST, then reflect the changes in the token stream.

See[START_REF] Krebbers | An operational and axiomatic semantics for non-determinism and sequence points in c[END_REF] for other examples of this kind.

Extract from the web page of Microsoft Visual C++ Refactoring (updated 5/2/2015) which is experimental: "The C++ language is large and complex with context-sensitive syntax subtleties that make it difficult to create a reliable and fast rename refactoring tool. [...] You might still need to manually go through unknown/unconfirmed results proportional to the scope of the refactoring for complex refactors, but for many common scenarios little intervention is required."

This could be relaxed with an analysis of the external library compiled code, but this is out of the scope of this report.

For instance, for that program, Visual Assist (Whole Tomato Software) for Visual Studio will perform the renaming of the global x into y, yielding a valid program from an invalid one, which obviously changes the semantics.

In this result, we use the bisimilarity between infinite traces defined in Compcert (traceinf sim) instead of Coq syntactic equality (see TraceProperties.behavior res eq).

The memory is unchanged at initialization, see theorem transforme init mem in module Memory.

A.1 Compcert State Invariants

We have identified five properties which are true on the continuations embedded in initial states (of the execution of the program) and that are preserved by transitions between states. Those invariants were needed to prove some properties on transformations of contexts and continuations.

• Local environments which are found in continuations are represented by trees which are in a canonical form (property PTreeProperties.canonique).

See Invariants.wf canonique invariant.

A.2 Higher Order Contexts

The concept of context is familiar in programming language semantics. It is used to specify places where computations can occur. In Compcert, contexts are represented by native Coq functions (type expr → expr), adopting the higher-order abstract syntax style [START_REF] Pfenning | Higher-order abstract syntax[END_REF]. Higher order data-structures have the well-known drawback of being difficult to inspect and transform.

To transform contexts, we flatten them by applying them to a witness/dummy value, which gives an expression, then we transform that expression, and then we build a function by embedding a substitution mechanism where the dummy values has the role of the placeholder for the formal parameter (see the module Contexts).

As a result, proofs on context transformations are more difficult to establish than proofs on transformations of "flat" structures such as expressions.

A.3 Bindings in Continuations

Bindings in continuations are more subtle than bindings in functions. Compcert continuations are "homomorphic" with lists (each continuation constructor has 1 or 0 continuation as parameter).

One of the constructors of continuations, Kcall, contains a function. That function binds parameters in all the continuation following that Kcall until the next Kcall. We call segment a part of a continuation delimited by Kcall constructors. So the bindings in a segment is fully determined by the bindings of the function in the Kcall constructor at the beginning of that segment.

However, the first segment of a continuation may not begin with a Kcall constructor. In this situation, the continuation does not contains enough information to determine the bindings in that first segment. The information for that segment is found elsewhere, for instance in the State construction that embeds that continuation.

For this reason, we provide two (mutually recursive) transformation functions for continuations : one that propagates the renaming on segments where the variable to be renamed is not masked (Continuations.change ident) and one for the other case, where nothing is transformed until the next segment (Continuations.skip).