Deepak Kapur

Invariant Generation as Semantic Unification: A New Perspective

Unification is the problem of finding instantiations of variables in a finite set of pairs of terms constructed using function symbols, such that the instantiated terms in each pair become equal. In semantic unification, also called E-unification, function symbols can have properties specified typically by an equational theory; a unifier then makes the instantiated pairs of terms equivalent modulo the equation theory. By generalizing the unification problem further, in which the pairs of formulas have variables ranging over formulas in a first-order theory, the invariant generation problem in software, hardware, and cyber-physical systems can be formulated as a unification problem. Finding a nontrivial unifier then amounts to finding an invariant. Similarly, finding a most general unifier, if unique, amounts to finding the strongest invariant. Instantiation of variables can be further restricted to formulas with certain shapes/properties. This new perspective is illustrated using a number of examples from the literature of the automatic generation of loop invariants in software.

Invariant Finding as Unification

The problem of unification in automated reasoning, logic programming, and Artificial Intelligence can be stated as follows: Let S be a finite set of pairs {⟨s i , t i ⟩ | 1 ≤ i ≤ k} of terms s i , t i built from a finite set X of variables and a finite set F of constants and function symbols. Check whether there exists a substitution/instantiation σ of variables in s i , t i 's such that σ(s i ) and σ(t i ) are identical for every i (referred to as the unifiability check), where σ(s i ), σ(t i ) are the results of applying the instantiation σ on variables in s i , t i . If S is unifiable, find a most general unifier (mgu) from which all unifiers can be generated. The problem can be further generalized to semantic or E-unification where the semantics of function symbols in F are specified as properties, typically as an equational theory E; in this case, a unifier σ should make σ(s i ) = E σ(t i ), where = E stands for equivalence modulo E. Higher-order unification extends this problem further to allow function and relation variables to occur in terms that can be appropriately instantiated.

At the University of New Mexico, I have been teaching in my course Semantics of Programming Languages for several years that the program invariant generation problem can be viewed as a unification problem. In this context, terms s i 's are formulas from a given theory that include formula variables standing for invariants/properties of programs; these formula, variables can be instantiated as formulas.

As illustrated below, a finite set of verification conditions are generated that are expressed using such formula variables, leading to a unification problem.1 Invariant generation is then to find substitutions for formula variables that make the instantiated verification conditions valid. A more detailed version of this extended abstract/summary is currently being prepared.

Consider a loop SL in a computation specified by a program, a hardware or cyber-physical system description, such as: SL: while b do S end A Hoare triple for the above loop is of the form:

{P } SL {Q}. Formulas P and Q are properties of interest for the loop. A Hoare triple specifies that if the program SL starts execution in a state satisfying a precondition P , and assuming SL halts, the program ends in a state satisfying a postcondition Q.

How does one determine (prove) the validity of the above Hoare triple? An intermediate formula called a loop invariant, denoted by I, capturing the partial semantics of the loop body S becomes essential. Using axiomatic semantics, the validity of the above Hoare triple can be decomposed into the following three conditions:

1.

P ⇒ I, 2. {(I ∧ b)} S {I}, 3. (I ∧ ¬b) ⇒ Q.
Conditions 1 and 3 are formulas, called verification conditions, while the second condition is still a Hoare triple. The process of associating variables standing for invariants is recursively applied on the loop body S, depending upon its structure, especially when S includes loops. For loop bodies that are sequences of assignment statements, condition 2 can be transformed into a verification condition.

Assuming condition 2 also transforms to one or more verification conditions which are formulas with I (and possibly other formula variables standing for other loop invariants), the above problem is a unification problem. The semantic properties of all symbols other than I and other formula variables, if any, are known. The goal is to find substitutions of I and other formula variables, if any, such that the resulting instantiation of each verification condition is valid. This is analogous to pairs of terms becoming equivalent after instantiation using a unifier.

It should be noted that the above formulation only allows for instantiations of I that are inductive invariants of the loop [START_REF] Falke | When is a formula a loop invariant? In Logic, Rewriting and Concurrency: Essays dedicated to Jose Meseguer on the Occasion of His 65 th Birthday[END_REF]; other loop invariants that are not necessarily inductive, can be found by strengthening as discussed in [START_REF] Falke | When is a formula a loop invariant? In Logic, Rewriting and Concurrency: Essays dedicated to Jose Meseguer on the Occasion of His 65 th Birthday[END_REF].

An Illustrative Example

Consider an example from [START_REF] Kapur | A quantifier elimination based heuristic for automatically generating inductive assertions for programs[END_REF] for computing the floor of the square root of a natural number.

{P } ⟨a, s, t⟩:=⟨0, 1, 1⟩; while s ≤ N do ⟨a, s, t⟩ :=⟨a + 1, s + t + 2, t + 2⟩; end while {Q} The axiomatic semantics of a simultaneous multiple assignments statement as a Hoare triple is a generalization of a simple (single) assignment statement.

{P } ⟨x 1 , . . . , x l ⟩ := ⟨e 1 , . . . , e l ⟩ {Q} if and only if (P ⇒ Q| ⟨e1,...,e l ⟩ ⟨x1,...,x l ⟩ ).

Here, Q| ⟨e1,...,e l ⟩ ⟨x1,...,x l ⟩ stands for the formula obtained from Q by simultaneously replacing all free occurrences of x 1 , . . . , x l by e 1 , . . . , e l , respectively. The variables x i 's are assumed to be distinct. 2The three conditions discussed above in this case are:

1. {P } ⟨a, s, t⟩:=⟨0, 1, 1⟩ {I}, which leads to the verification condition: 1 ′ . P ⇒ I| ⟨0,1,1⟩ ⟨a,s,t⟩ .

2. {I ∧ s ≤ N } ⟨a, s, t⟩ :=⟨a + 1, s + t + 2, t + 2⟩ {I} from which the verification condition generated using backward semantics is:

2 ′ . (I ∧ s ≤ N ) ⇒ I| ⟨a+1,s+t+2,t+2⟩ ⟨a,s,t⟩ .
As in the case of an expression above, I| ⟨a+1,s+t+2,t+2⟩ ⟨a,s,t⟩ is the formula obtained from I after simultaneously replacing a, s, t by a + 1, s + t + 2, t + 2, respectively.

The third condition is simply 3 :

(I ∧ ¬(s ≤ N )) ⇒ Q. If Q is known, then it is that specific formula; otherwise, Q is a formula variable.
Similarly, if a precondition P is not known, then it is also a formula variable.

In the above example, a goal for the partial correctness of the above program is to find an instantiation α(a, s, t, N ) of the loop invariant variable I, a formula in input parameters (if any), output parameters (if any), and program variables, as well as for P and Q if they are not known/given, such that these instantiations make the first two verification conditions valid. The instantiation for the postcondition Q can be taken to be any formula implied by α(a, s, t, N ) ∧ ¬(s < N ), particularly the formula α(a, s, t, N ) ∧ ¬(s < N ) itself.

It is easy to see that I being true satisfies the above conditions. However, this trivial invariant does not provide any useful information about the program's behavior.

Trying to find nontrivial substitutions for I, it can be proved that I being t = 2a + 1 and/or s = -a 2 + at -a + t and/or 4s = t 2 -2a + 3t satisfy the above three conditions. From the conjunction of these substitutions, the equation s = (a + 1) 2 is implied. It is not a solution to the above unification problem, but its strengthening s = (a + 1) 2 ∧ t = 2a + 1 is a solution. Using this substitution, one gets the postcondition s = (a + 1) 2 ∧ t = 2a + 1 ∧ s > N , which specifies an approximation to the behavior of the above program.

Observe that a nontrivial solution to the unification problem as formulated above not only gives a loop invariant but also a partial specification of the program. Similarly, a precondition under which a program satisfies its postcondition can be derived from an invariant generated as a unifier.

In the presence of a specific postcondition, the third condition (I ∧ ¬b) ⇒ Q constrains possible unifiers. For the above example, a possible postcondition can be s = (a + 1) 2 ∧ (a + 1) 2 > N ≥ a 2 , in which case many of the unifiers for the case where Q is formula variable, are no more any unifiers as they are unable to satisfy the third condition. Notably, true, t = 2a + 1, or s = (a + 1) 2 are no longer unifiers. Any unifier must imply the inequality N ≥ a 2 .

Since a precondition and a postcondition can be arbitrary first-order formulas, the validity problem of first-order logic can be reduced to the above unification problem, showing that the problem is in general undecidable.

Constraining Unifiers over a Theory

Let T be a first-order theory associated with a language L consisting of a finite set of predicate and function symbols. Formulas are constructed in the usual way using a finite set X of variables ranging over the domain(s) of the discourse of T . Let F T stand for the formulas in L. To distinguish from the variables in X, include a finite set of new variables ranging over formulas in T . The new variables are called formula variables and can be used in the same way as formulas to construct extended formulas which include occurrences of formula variables; extended formulas without formula variables are regular formulas. We will abuse the terminology and unless needed, will not make any distinction between extended formulas and formulas.

Given a finite set S of extended formulas {α i |1 ≤ i ≤ m} involving formula variables I j , the unifiability problem is to decide whether there exists a substitution σ for formula variables so that each instantiated formula σ(α i ) is valid in T . 3For the above example, formula variables range over the first-order number theory (Peano Arithmetic), which defines the semantics of other symbols such as 0, s, +, * , ≥. Typically T is desirable to be a decidable theory. If the postcondition in the example is weakened to include only symbols from Presburger arithmetic, then the above unification problem can be solved over that theory. It is also possible to consider an even weaker theory, such as the theory of conjunctions of linear equations over integers. In many such cases when unifiers are restricted to be in a subtheory, the unification problem can be shown to be decidable. This perspective relates to the abstract interpretation framework for generating invariants as discussed in the next subsection; see also section 6.

Approximation/Abstraction of Verification Conditions

When substitutions for formula variables are restricted to be in a subset of F T , in other words, unifiers are restricted, the verification conditions in S must be approximated to a new problem S ′ that soundly approximates S in the sense that any solution σ of S ′ is also a solution of S with the extra symbols not in S ′ being viewed as uninterpreted.

The above example also illustrates the perspective of approximating formulas in S that include occurrences of <, ≥,, etc. If the postcondition Q for the above example is a particular formula s = (a + 1) 2 , one can restrict the unification problem in which the formula variables are restricted to be a conjunction of polynomial equalities.

The first condition which includes ≥, can be soundly approximated as: 1 ′ true ⇒ I| ⟨0,1,1⟩ ⟨a,s,t⟩ . The second condition soundly approximates to: 2 ′ . I ⇒ I| ⟨a+1,s+t+2,t+2⟩ ⟨a,s,t⟩ .

And the third condition is: 3 ′ : I ⇒ s = (a + 1) 2 .

It can be shown that I can be instantiated as t = 2a + 1 ∧ s = (a + 1) 2 , which is thus a unifier. 4 This substitution is also a unifier for the original problem in which the verification conditions are expressed using <, ≥,, etc.

Another way to approximate invariant generation as a unification problem is illustrated using an example from a classical paper by Cousot and Halbwachs [START_REF] Cousot | Automatic Discovery of Linear Restraints among Variables of a Program[END_REF] on the polyhedral abstract domain. Conditions/Boolean tests not included in a theory are replaced by formula variables whose substitutions can be restricted to be true. The negations of P 1 and P 2 for the loop exit condition and the if . . . then . . . else statement, respectively, are also restricted to be true to ensure all paths are considered. ⟨i, j⟩:=⟨2, 0⟩; while P 1 do if P 2 then ⟨i, j⟩:=⟨i + 4, j⟩; else ⟨i, j⟩:=⟨i + 2, j + 1⟩; end if end while From various program paths, the verification conditions generated leading to a unification problem are as follows:

1. (i = 2 ∧ j = 0) ⇒ I, 2. (I ∧ P 1 ∧ P 2 ) ⇒ I| ⟨i+4,j⟩ ⟨i,j⟩ 3. (I ∧ P 1 ∧ ¬P 2 ) ⇒ I| ⟨i+2,j+1⟩ ⟨i,j⟩ .
The postcondition is expressed as a formula variable Q: 4. (I ∧ ¬P 1 ) ⇒ Q.

The above unification problem has nontrivial invariants, including j ≥ 0 as well as i ≥ 2j + 2. As stated earlier, all unspecified symbols including P 1 , P 2 , ¬P 1 , ¬P 2 are assumed to be true, representing their weakest possible semantics.

It is also possible to restrict considering substitutions expressed only in certain variables. Such restrictions can be helpful in simplifying unification algorithms.

Unification Problems arising from Multiple Loops

As is well-known, for a simple programming language with loops, assignments, conditional statements, and sequencing of statements, it suffices to associate a loop invariant with each loop. Besides formula variables for a precondition and a postcondition, if not specified, the resulting unification problem can have multiple formula variables for each loop.

Consider another related example from [START_REF] Kapur | A quantifier elimination based heuristic for automatically generating inductive assertions for programs[END_REF]:

{P } ⟨m, n, s, x⟩:=⟨0, 0, 0, N ⟩; while x ̸ = 0 do ⟨x, n, m⟩:=⟨x -1, m + 2, m + 1⟩; while m ̸ = 0 do ⟨s, m⟩:=⟨s + 1, m -1⟩; end while m:=n; end while {Q} Let I and J, respectively, stand for formula variables associated with the outer loop and inner loop. Corresponding to various paths in the program, the following verification conditions are generated:

P ⇒ I| ⟨0,0,0,N ⟩ ⟨m,n,s,x⟩ . (I ∧ x ̸ = 0) ⇒ J| ⟨x-1,m+2,m+1⟩ ⟨x,n,m⟩
for the path from the outer loop entry to the inner loop entry. The path corresponding to the body of the inner loop gives: (J ∧ m ̸ = 0) ⇒ J| ⟨s+1,m-1⟩ ⟨s,m⟩ . And, (J ∧ m = 0) ⇒ I| n m is the verification condition corresponding to the path from the exiting of the inner loop to the end of the outer loop body. Finally, upon exiting the outer loop, the verification condition is (I ∧ x = 0) ⇒ Q.

If I and J are constrained to be conjunctions of linear equalities, then it can be shown that I : m = 2N -2x ∧ m = n and J : n = 2N -2x are unifiers. These are indeed invariants of the respective loops under the assumption that P is instantiated to be true and Q is I itself.

In Presburger arithmetic, more general unifiers including m ≥ 0, n ≥ 0, s ≥ 0, x ≥ 0, can also be derived.

If I and J are conjunctions of polynomial equalities and atomic formulas expressing simple inequalities such as m ≥ 0, n ≥ 0, then the above unifiers can be made even more general to include conjunctions of the set of formulas:

{m ≥ 0, n ≥ 0, s ≥ 0, x ≥ 0, m = 2N -2x, m = n, N 2 -x 2 = s + mx} in I under the assumption that P is instantiated to be N ≥ 0.
Similarly, J is the conjunction of the set of formulas:

{ m ≥ 0, n ≥ 0, s ≥ 0, x ≥ 0, n = 2N -2x, N 2 -x 2 = m + s + n x}. 5
4 Invariants/Unifiers form a Lattice with Implication as Ordering

It is easy to prove that if α 1 and α 2 are two unifiers of the verification conditions with formula variables, then α 1 ∧ α 2 as and α 1 ∨ α 2 are also unifiers. Furthermore, if α is a unifier, then so is any formula β such that α ⇒ β. In short, the unifiers of the above problem form a lattice using implication as the ordering. In case a precondition and a postcondition are not specified, i.e., they are also formula variables, then true is typically the least element of the lattice, and the strongest unifier corresponding to the strongest invariant is its greatest element.

In the presence of a postcondition, the lattice of unifiers/invariants is constrained by the postcondition; as was illustrated by examples above, some of the formulas that are unifiers/invariants in the absence of a postcondition are not invariants. The lattice of unifiers then has as its least element being the weakest unifier corresponding to the weakest invariant in implication ordering as constrained by the precondition and postcondition. The greatest element still represents the strongest unifier corresponding to the strongest invariant, and need not be constrained by the postcondition.

If unifiers are restricted to be from a subclass of formulas, the lattice of unifiers is the formulas from the subclass with implication relation among them.

Unification Algorithms

How does one solve such unification problems? In [START_REF] Kapur | A quantifier elimination based heuristic for automatically generating inductive assertions for programs[END_REF], the quantifier elimination-based approach is discussed in depth for solving some of the above unification problems.

If verification conditions are abstracted to be a conjunction of polynomial equalities and disequalities, implying a conjunction of polynomial equalities, then the unification problem can be transformed into a problem on ideals and their associated varieties. Gröbner basis algorithms can be useful for developing unification algorithms for such cases; see [START_REF] Rodríguez-Carbonell | Automatic Generation of Polynomial Invariants for System Verification[END_REF][START_REF] Rodríguez-Carbonell | Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations[END_REF].

If unifiers are restricted to be of a certain shape or have some properties, then a template-based approach presented in [START_REF] Kapur | A quantifier elimination based heuristic for automatically generating inductive assertions for programs[END_REF] can be used for solving the unification problems. This involves hypothesizing a unifier as a template with parameters; from verification conditions to be valid, constraints on parameters are generated. A solution to the parametric constraints after substituting in the template solves the unification problem. Such solutions can be automatically generated using SMT solvers, particularly those solvers which have extensions for synthesizing programs.

In [START_REF] Falke | When is a formula a loop invariant? In Logic, Rewriting and Concurrency: Essays dedicated to Jose Meseguer on the Occasion of His 65 th Birthday[END_REF], an iterative/fixed-point algorithm is given for solving the above problem under the assumption that an approximate unifier is already known. A unifier σ is called approximate if it does not solve the unification problem but there exists a strengthening δ of σ such that δ ⇒ σ and δ is a unifier. Typically, δ is obtained by a conjunction of σ with additional atomic formulas generated by the iterative algorithm in its attempt to compute strengthening leading to a unifier.

There are thus many opportunities for developing new unification algorithms when theories are restricted and/or formulas to serve as instantiations for formula variables can only be expressed using certain program variables and/or have a certain shape.

Relation to Abstract Interpretation

We conjecture that the above framework encompasses abstract interpretation frameworks, where unifiers/formulas are from an abstract domain such as:

• An interval domain in which formula variables are instantiated to be conjunctions of atomic formulas of the forms x ≤ h and l ≤ x, where x is a program variable and l, h are integers or ±∞, or

• an octagonal domain, in which formula variables are instantiated to be conjunctions, including the constraints of the maximum and minimum values on each program variable as well as maximum and minimum values of x + y, x -y for every pair of distinct program variables x, y, or

• a polyhedral domain in which formula variables range over a conjunction of linear inequalities.

To solve the verification conditions generated from the semantics of programs, sound approximations may be necessary to get a unifier in the specified domain. Defining an abstraction function and transfer functions on abstract values implementing the operations used in a program is a systematic way to formulate sound approximations to a unification problem such that a solution to the approximate problem is also a solution to the original problem. In [KZH + 13], an approach is discussed on how verification conditions can be approximated when invariants are expressed as conjunctions of octagonal constraints. More work is needed to study the relationship between the Abstract Interpretation framework and the proposed formulation of automatic invariant generation.

Challenges

There are numerous challenges in viewing an invariant generation problem as a unification problem in theories. Some of these include:

• Developing support for richer data structures such as arrays, pointers, lists, and other containers, as well as other control structures, as long as their axiomatic semantics can be given, leading to the generation of their verification conditions possibly using formula variables.

• Expanding the family of theories on which unification problems formulated for invariant generation can be solved.

• Exploring approximate sound unification problems that lead to generating a unifier for the original problem but are restricted to a formula in a subtheory and/or of a certain shape.

Since the second component of pairs in this problem is always true, it is omitted.

If Q is not quantifier-free, substitutions should be performed carefully to avoid the free variables appearing in e i 's being captured by the scope of quantifiers in Q; to avoid that, quantified variables may need to be renamed. For simplicity, Q is assumed to be quantifierfree.

In this formulation of the unifiability problem, the second component in the pair of formulas is always assumed to be true and is thus omitted.

 4 It is easy to see that s = (a + 1) 2 alone is not a unifier since it is not an inductive invariant of the loop; see[START_REF] Falke | When is a formula a loop invariant? In Logic, Rewriting and Concurrency: Essays dedicated to Jose Meseguer on the Occasion of His 65 th Birthday[END_REF].

Invariants reported of a related program in[START_REF] Kapur | A quantifier elimination based heuristic for automatically generating inductive assertions for programs[END_REF] have quite a few typos, for which I apologize.

Acknowledgment: Thanks to Jose Abel Castellanos-Joo for his comments while proofreading this extended abstract.


Rezzoug Sid-Ahmed

Janocka Ingrid

Influence of instantaneous controlled pressure drop extraction conditions on

Keywords: Maritime pine (pinus pinaster), extraction, vacuum, essential oil, D.I

teaching and research institutions in France or abroad, or from public or private research centers.

Influence of instantaneous controlled pressure drop extraction conditions on composition and oil yield from

Maritime Pine (Pinus Pinaster)

Sid-Ahmed Rezzoug, Ingrid Janocka

To cite this version:

Sid-Ahmed Rezzoug, Ingrid Janocka. Influence of instantaneous controlled pressure drop extraction conditions on composition and oil yield from Maritime Pine (Pinus Pinaster). 11ème Congrès de la Socité Française de Génie des Procédés -SFGP 2007, Oct 2007, Saint-Etienne, France. pp.Rezzoug. hal-00414529

Introduction

Essential oil is any class of volatile oil composed of a mixture of complex hydrocarbons (mainly terpenes) and other chemicals isolated from plants. One of their characteristics is the generation of flavour or aroma. Essential oils extracted from plants as pine are widely used as fragrances in cosmetics, flavouring additives of foods and beverages, scenting agents in a variety of household products as detergents, soaps or insect repellent. They are also used as intermediate in the synthesis of perfume chemicals and often sold for unconventional medicinal purposes as well as in aromatherapy (Lazutka et al., 2001). The conventional methods for the extraction of the essential oils have some disadvantages. For the steam distillation and hydrodistillation, the elevated temperatures can cause chemical modifications of the oil components and often a loss of the most volatile molecules (Khajeh et al., 1997). When using the solvent extraction, it is impossible to obtain a solvent-free products and this process usually results also in the loss of the highly volatile components. In contrast, extraction by supercritical fluids leads to highquality and solvent-free extracts (Reverchon, 1997). However, according to Temelli et al., (1988) and to Oszagyan et al., (1996) the technological conditions required for the use of supercritical fluids are onerous and the high cost of producing specific products has limited its use. Moreover, several studies have shown that the CO 2 not only extracts the essential oil, but also other compounds such as vegetable waxes or resins. The Instantaneous Controlled Pressure Drop process, known as "D.I.C", was developed in our laboratory some years ago [START_REF] Rezzoug | 10 èmes Rencontres Scientifiques et technologiques des Industries Alimentaires[END_REF], initially for use in the field of the drying-texturation of various food products by improving the hydration capacity. This process is based on the thermo-mechanical processing induced by subjecting the product to a rapid transition from high steam pressure to a vacuum.

In the case of food products such as vegetables, the aim was to improve the vaporization of water with a preservation of the fragrance coupled to an alveolate texture of dried product while in this paper, we used this process in order to separate the volatile oil from the solid material. The essential oil isolation based on this process, which was successfully tested for isolation of essential oil from orange peels (Rezzoug et al., 2000a) is an interesting alternative not only to standard techniques of essential oil extraction, such as extraction with solvents or steam distillation, but also to more effective processes such as those using the supercritical fluids. In fact, this extraction process does not require the use of any solvent and the induced cooling when the plant is rapidly transferred from a high steam pressure to a vacuum stops all thermal degradation of the essential oil components (Rezzoug et al., 2005). The processing by instantaneous controlled pressure drop increases the global diffusivity of the product and improves the availability of the liquid in the plant. In this contribution, this process was used to extract the volatile oil from maritime pine (pinus pinaster). Two processing parameters of this process were evaluated: the processing pressure and the processing time. The response parameters were the global extraction yield of essential oil as well as the variation of the yield of 3 important qualitative molecules namely α-pinene, β-pinene and germacrene D.

Materials and methods

Plant material

Maritime pine (Pinus Pinaster) was collected from plants growing in west southern France. The leaves were used at their residual moisture content (63.1 % by weight on dry basis). Some experiment were also performed on dried needles (40 % and 10 % by weight on dry basis) Vacuum container -5. Vacuum pump -6. Extract container.

Experimental set-up

The experimental set-up (fig. 1) was largely described in a previous study (Rezzoug et al., 2005); it is composed of three main elements → The processing vessel (2) where the samples were placed and treated.

→

The vacuum system which consists mainly from a vacuum tank (4) with a volume (360 l) 130 fold greater than the processing vessel (12 l), and a vacuum pump (IV). The initial vacuum pressure of the vacuum container was maintained at 50 mbar in all the experiments.

→

A pneumatic valve (3) that separate the processing vessel from the vacuum tank. It can be opened in less than 0.2 seconds; this ensures a rapid decompression within the reactor.

Protocol of extraction by the instantaneous controlled pressure drop process

The needles are firstly placed in the D.I.C vessel (fig. 1-2) which is maintained under a vacuum (~ 50 mbar) through its connection to a vacuum container (fig. 2a). The vacuum allows a better diffusion of the heating fluid through the plant and consequently heat transfer between the steam and wood is improved and the time to reach the desired processing pressure (or processing temperature) is shortened. After closing the electropneumatic valve (fig. 123) which connects the reactor to the vacuum tank (Fig. 1234), an atmosphere of steam pressure (between 1 and 6 bar) is created within the D.I.C. reactor (fig. 2c). After a processing time at fixed processing pressure (fig. 2d), the thermal treatment is followed by a rapid decompression resulting in a rapid drop in pressure (fig. 2e). The equilibrium pressure after decompression depends on the operating pressure: the higher the processing pressure, the higher the equilibrium pressure. The evaporation, which is effected in adiabatic conditions, induces a rapid cooling of the residual product. The final temperature must be commensurate with the final pressure. The maritime pine wood extract and the condensed steam are recovered in a specific container (Fig. 123456). The volume of the obtained mixture was about 400 ml for all experiments. 2.4 Steam distillation 50 g of maritime pine needles chips were placed on stainless steel grid. This grid was disposed in a glass chamber containing boiling water. The steam crossed the grid during two hours and was recovered in condensate form with volatiles compounds after crossing a refrigerant. The condensates were separated into aqueous phase and organic phase (essential oil) by decantation.

GC/MS conditions

Varian 3900 gas chromatograph coupled to a Varian Saturn 2100T ion trap mass spectrometer (Varian, France) for characterizing the extracts was used. The column was a 30m × 0.25 mm, 0.25 µm CP-Sil 8 CB Low Bleed MS capillary column (Varian, France). Column temperature was 80°C (3min) -3°C/min -250°C (40 min). We used Helium as carrier gas at 1 ml/min. The extract samples were injected via a Varian CP-8400 autosampler fitted with a 5µl syringe. Transfer line temperature was 280°C. Electron ISBN 2-910239-70-5, Ed. SFGP, Paris, France impact mass spectra were obtained at 70 eV ionization potential and peak identity was identified by NIST 2002 Data library.

Results and discussion

The compounds identified and their yield are shown in table 1. The yield of essential oil in fresh raw material was 0.82 % by mass (g of E.O/100 g dm). This value is in agreement with the value cited by authors like Kelkar et al., (2006) and Dob et al., (2005).

Effect of drying of maritime pine needles before Instantaneous Controlled Pressure Drop process on extraction efficiency

To evaluate the effect of drying (in an oven at 25 °C) on the composition of the essential oil extract, experiments of extraction by steam distillation were carried out on three samples of maritime pine needles. The first one on fresh product, the second one on needles dried to 40 % moisture content (d.b) and the third experiment on needles dried to 10 % moisture content (d.b). The results are grouped in table 2. It clearly appears that the global extraction yield diminishes with the moisture content as well as the concentration of the majority of molecules. For the most important one the yield decreased from 40.5 for fresh needles to 22.5 % (g of molecule / 100 g essential oil) for needles dried to 10 % moisture content (d.b). This can be explained by an evaporation of a part of the molecule during the drying. For some molecules as β-caryophillene, an increasing of the yield was observed. It can be explained by a total disappearance of some molecules which leads to an augmentation of the concentration of the identified molecules. So for the extraction by instantaneous controlled pressure drop process, the needles were treated at fresh state (~63 % d.b). A parametric study was performed by varying two process parameters of the instantaneous controlled pressure drop process. The variations of process parameters are summarized in table 2. The processing pressure was varied from 1 to 5 bar, the initial and the processing time from 1 to 35 minutes. The validity of the results was confirmed by the low uncertainty limit in the extraction yield (based on 1.35 % error estimate) obtained from eight replications at processing pressure of 4 bar and processing time of 4 minutes. ISBN 2-910239-70-5, Ed. SFGP, Paris, France

Effect of processing pressure on global extraction yield and on the yield of the three selected qualitative molecules

In the first variation, the processing time was fixed at an acceptable value of 4 minutes as contact time between the raw material and saturated steam at different temperatures corresponding to a processing pressure variation from 1 to 6 bar. It should be noted that steam distillation at industrial scale is performed in two from three hours. Chen and Spiro (1994) who worked on microwave extraction of essential oil from rosemary leaves reported that a long time at high temperatures could cause rearrangement or polymerization of some of rosemary oil constituents which are close to the constituents present in the needles of maritime pine oil. Figure 4 show that the processing pressure has a significant effect on extraction efficiency. When the processing pressure increases from 1 to 4 bar, the extraction yield increases from 0.25 to 1.75 %. Beyond 4 bar, a weak variation was observed and yield stabilize about 2 % (d.b) from 5 bar processing pressure. The drop of steam pressure from 3-5 bar to vacuum caused a mechanical strain, which had as effect a degradation of the glands containing the volatile molecules. The same observation was cited by Chen and Spiro (1994), who reported that the oil synthesized in the secretory cells was not released unless an external factor damages the gland. This observation was also verified by Boutekedjiret et al., (2004), whom compared the isolation of rosemary oil by different extraction processes, including the Instantaneous Controlled Pressure Drop Process. The authors observed by scanning electron microscopy, that the microstructure of rosemary leaves after extraction were more expanded with appearance of cavities indicating a partial collapse of the leaf structure. The processing pressure was therefore maintained at 4 bar in processing time variation experiments. This results shows that compared with other "flash" extraction processes, extraction by D.I.C is more efficient and thus at industrial level, a subsequent steam distillation step is not necessary.

From industrial point of view, the qualitative criterion of maritime pine extracts is based on the presence of three molecules namely α-pinène, β-pinène and germacrene D, in defined percentage in the essential oil as commercial standards. The α-pinene must represent between 33 and 43 % of the extract, β-pinene between 22 and 32 % and germacrene D between 0.5 and 4 % of the oil. For this reason, the effect of processing pressure of DIC extraction process on the quantity of these molecules was studied.

From figure 5 (a), it can be seen that when the processing pressure increases from 1 to 2 bar, the yield of α-pinene slightly increase from 41 to 41.3 % and remains almost stable up to 4 bar. Beyond this value of processing pressure, an important diminution of α-pinene yield was observed, from 40.8 at 4 bar to 37.5 at 6 bar. This clearly indicates a certain degradation of this molecule occurs when the processing exceeds 4 bar. For β-pinene, which is also an important molecule in the maritime pine needles oil, it can be seen from figure 5 (b), that 90 % of this molecule is extracted at 2 bar (at 4 minutes processing time). Beyond this processing pressure, a very weak variation of β-pinene yield is observed. Figure 5 (c) indicates the effect of processing pressure on the yield of germacrene D. It can be seen that the behavior is different to that of the two first molecules. In fact, the yield is stable about 1.5 and 1.8 g of germacrene D/100 g of essential oil, for processing pressures ranged between 1 and 3 bar. Over this value, the yield of germacrene D increases from 1.8 to 4.6 g of molecule /100 g of essential oil. We can therefore argue that the proposed process is selective. If we favor the presence of monoterpenes hydrocarbons in the maritime pine extract, it would be better to work at processing pressure included between 2 and 4 bar. In contrast, if we favor the presence of germacrene D, processing pressures more than 4 bar are more suitable.

Effect of processing time on global extraction yield and on the yield of the three selected qualitative molecules

For the variation of processing time, the processing pressure was maintained at 4 bar. It can be seen from figure 6 that at this processing pressure, 4 minutes are sufficient to extract more than 80 % of available essential oil. The maximum of extraction yield is almost reached after 8 minutes processing time. Beyond this value, a certain degradation of isolated oil, expressed by a more deepened coloring was observed. By looking figure 6 more closely, we can observe that the yield evolution versus processing time show a very rapid increase during the first minutes of the isolation process, then gradually levelled to the equilibrium value at the end of the process. The kinetic plot is similar to that obtained for rosemary leaves oil extracted by instantaneous controlled pressure drop process (Rezzoug et al 2000b). For the variation of processing time, the processing pressure was maintained at 4 bar. It can be seen from figure 6 that at this processing pressure, 4 minutes are sufficient to extract more than 80 % of available essential oil. The maximum of extraction yield is almost reached after 8 minutes processing time. Beyond this value, a certain degradation of isolated oil, expressed by a more deepened coloring, was observed. By looking figure 6 more closely, we can observe that the yield evolution versus processing time show a very rapid increase during the first minutes of the isolation process, then gradually levelled to the equilibrium value at the end of the process. The extraction of the oil from maritime pine needles, by instantaneous controlled pressure drop process, seems to be regulated by two distinct phenomena corresponding to two steps. The first one is rapid compared to the second. It corresponds to a free diffusion phenomenon which takes place at the plant surface. On the other hand, the rapid decrease in the extraction rate observed from 5 min processing time may be due to endogenous stockage sites of the oil. The oil recovered in the second step is probably regulated by osmosis phenomena and slow diffusion through the plant cells towards the surface. However it can be seen that the oil collected in the last step (~6 %) is very low compared to the first step (~94 %). It is obvious that the major part of the oil is recovered by a simple process of free diffusion and evaporation. The proportions of these two parts for steam distillation extraction are generally lower for the first step and higher for the last one. This difference may be attributed to the presence of saturated steam under pressure in the case of instantaneous controlled pressure drop process that allows reaching more endogenous sites than at atmospheric pressure in the case of steam distillation. For the three studied molecules, the processing time have also a significant effect. The previous observation is clearly confirmed for one of the two monoterpene hydrocarbons i.e β-pinene as well as germacrene D (figures 7(b) and (c)). For these essential oil compounds increasing of processing time leads to an increasing of their yield, essentially between 1 and 20 minutes. For β-pinene, 1 minute is sufficient to extract more than 60 % from the total of this compound and to extract the totality; 10 to 12 minutes are required. The germacrene D, which is considered as a precursor of many sesquiterpene hydrocarbons, exhibit the same behaviour as β-pinene. When the processing time increases from 1 to 35 minutes, the yield varied from 1.37 to 2.61 g of germacrene D/100 g of essential oil. For these two molecules, the variation of the yield has two phases. The first one from 1 to 10-12 minutes and the second one from 12 to 35 minutes. As for the global extraction yield, the first phase is more rapid than the second one. An inverse trend is observed for α-pinene. Increasing of processing time induced a decreasing in its yield, indicating also here a certain degradation of this molecule which is the more volatile. Commelli et al., (2006) reported a same behaviour for the isomerization reaction of α-pinene which produces bicyclic and monocyclic compounds and other products, in presence of catalyst and temperature.

Conclusion

The aim of this work was to provide an efficient and economically attractive process for extraction of oil from maritime pine (pinus pinaster) needles. This recent extraction process was also successfully tested on isolation of oils from other plants such as citrus. The developed extraction process is an interesting alternative not only to standard techniques of essential oil extraction, such as extraction with solvents or steam distillation, but also to more effective processes such as those using the supercritical fluids. This method doesn't require the use of a solvent and has the advantage of being both fast and selective. Among operative parameters of the instantaneous controlled process, we varied 2 parameters in this work: the processing pressure and the processing time. The conducted parametric study showed that the optimum extraction conditions in the studied ranges are a 4 bar steam pressure for 8 minutes. Unfortunately, for this value of processing time a certain degradation of α-pinene was observed and if the aim is to favor the presence of this molecule to the detriment of the global extraction yield, the processing time must be reduced to 4 minutes. The energy consumption and the flexibility of the proposed process can be favourably compared with other methods because the processing time was reduced from more than 2-4 hours hour to 4-8 minutes.

Figure. 1

 1 Figure.1 Schematic diagram of the apparatus used for the extraction of essential oil from rosemary leaves by Controlled Instantaneous Decompression. 1. Boiler -2. Treatment vessel (made of stainless steel ) -3.Valve -4.Vacuum container -5. Vacuum pump -6. Extract container.

Figure 2 :

 2 Figure 2: Typical pressure-time profile for DIC processing cycle. (a) sample at atmospheric pressure; (b) establishment of vacuum; (c) steam injection to reach selected pressure; (d) treatment time at selected processing pressure; (e) pressure drop; (f) atmospheric pressure for the sample recovery

Figure 3 :

 3 Figure 3: Effect of drying of maritime pine needles on the yield of essential oil extracted by steam distillation

Figure 4 :

 4 Figure 4: Effect of processing pressure in Instantaneous Controlled Pressure Process on the extract yield

Figure 5 :

 5 Figure 5: Effect of processing pressure in Instantaneous Controlled Pressure Process on the yield of 3 important molecules of maritime pine essential oil. (a): α-pinene; (b): β-pinene; (c) germacrene D. In all experiments, the processing time is fixed at 4 minutes.

Figure 6 :

 6 Figure 6: Effect of processing time in Instantaneous Controlled Pressure Process on the extract yield

Figure 7 :

 7 Figure 7: Effect of processing time in Instantaneous Controlled Pressure Process on the yield of 3 important molecules of maritime pine essential oil. (a): α-pinene; (b): β-pinene; (c) germacrene D. In all experiments, the processing pressure is fixed at 4 bar.

Table 1

 1

	. Percentage composition of fresh pinus pinaster needles oil
	isolated by steam distillation
	Constituents	g/100 g of E.O
	Tricyclene	0.08
	α-Pinene	40.50
	camphene	0.75
	β-pinene	25.42
	β-myrcene	3.61
	p-cymene	4.02
	limonene	3.52
	γ-terpinene	0.08
	dehydro p-cymene	0.07
	terpinolene	0.74
	4-terpineol	0.21
	α-terpineol	1.05
	α-copaene	0.40
	longifolene	1.92
	β-caryophillene	6.30
	α-humulene	1.08
	germacrene-D	3.21
	g-cadinene	1.09
	Caryophillene oxyde	0.29

Table 2 .

 2 Percentage composition (in g of molecule 100 g of essential oil) of pinus pinaster needles oil dried at two different moistures contents: 10 % and 40 % (d.b)

	Constituents/ Moisture content	40 %	10 %
	Tricyclene	0.059	0.06
	α-Pinene	28.91	22.52
	camphene	0.863	0.640
	β-pinene	15.52	13.32
	β-myrcene	1.571	1.012
	p-cymene	0.015	0.014
	limonene	2.994	2.424
	γ-terpinene	0.141	0.175
	dehydro p-cymene	0.033	0.021
	terpinolene	0.902	0.765
	4-terpineol	0.085	0.064
	α-terpineol	0.735	0.413
	α-copaene	1.005	0.912
	longifolene	3.114	4.853
	β-caryophillene	6.748	9.882
	α-humulene	1.496	1.801
	germacrene-D	2.328	1.758
	γ-cadinene	1.775	2.059
	Caryophilene oxyde	1.503	1.295

Table 3 .

 3 Processing parameters performed in the parametric study of maritime pine oil extraction by instantaneous controlled pressure drop process

	Processing pressure (bar)	Processing time (min)
	1	1
	2	2
	3	4
	4	8
	5	12
	6	20
		35
	processing time = 4 min *	processing pressure = 4 bar *

* Fixed processing parameters in each parametric study