Pure function aspect?...

Pure function aspect?...

[Martin]

Now Ada has bitten the bullet and allowed "in out" mode parameters in
functions, is it time to allow users to contract the other extreme and
allow a function to be declared Pure (no state changes, not even
hidden ones)? e.g.

package P is
   type T is tagged private;
   function Pure_F   (Self : T) return Integer
      with Pure;
   function Impure_F (Self : T) return Integer;
private
   type T is tagged record
      I : Integer := 0;
   end record;
end P;


Functions with a Pure contract would be allowed to call other
functions with pure contracts, read values/parameters but promise to
change nothing (not even via 'tricks' a la random number generator!!).

-- Martin

Re: Pure function aspect?...

[Randy Brukardt]

"Martin" <martin@thedowies.com> wrote in message 
news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com...
> Now Ada has bitten the bullet and allowed "in out" mode parameters in
> functions, is it time to allow users to contract the other extreme and
> allow a function to be declared Pure (no state changes, not even
> hidden ones)? e.g.
>
> package P is
>   type T is tagged private;
>   function Pure_F   (Self : T) return Integer
>      with Pure;
>   function Impure_F (Self : T) return Integer;
> private
>   type T is tagged record
>      I : Integer := 0;
>   end record;
> end P;
>
>
> Functions with a Pure contract would be allowed to call other
> functions with pure contracts, read values/parameters but promise to
> change nothing (not even via 'tricks' a la random number generator!!).

We've argued this for a long time within the ARG, and we haven't been able 
to get a real consensus. This discussion goes back to Ada 79 (which is even 
before I got involved in Ada) -- early drafts of Ada had both functions 
(which were what we now call pure) and value-returning procedures (which 
were not). The concern was that there was not a clear line between them, and 
moreover there are many sorts of functions that are "logically" pure but 
still do change things (the "memo function" being the banner carrier for 
that idea).

Personally, I would be happy to have strong checks on such functions, and I 
don't much care about what gets left out (it's not that important, and any 
such functions are not task-safe anyway, so it is already a good idea to 
avoid them in Ada code). But not everyone agrees. We just had another 
version of this discussion in Denver; we ended up adopting an undetectable 
bounded error for this case (in the case of assertions, including 
preconditions, et. al.).

I had tried an alternative approach for Ada 2012, by suggesting the addition 
of checked global in/out contracts to subprograms. Eventually, this was 
dropped from Ada 2012 as being insufficiently mature. My understanding is 
that AdaCore is experimenting with a version of it in their formal methods 
research, so it isn't necessarily gone forever (which is good, considering 
the amount of time I put in on it). You can see the last proposal at 
http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0186-1.txt.

                                                             Randy.

Re: Pure function aspect?...

[Dmitry A. Kazakov]

On Thu, 12 Jan 2012 18:00:05 -0600, Randy Brukardt wrote:

> "Martin" <martin@thedowies.com> wrote in message 
> news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com...
>> Now Ada has bitten the bullet and allowed "in out" mode parameters in
>> functions, is it time to allow users to contract the other extreme and
>> allow a function to be declared Pure (no state changes, not even
>> hidden ones)? e.g.
>>
>> package P is
>>   type T is tagged private;
>>   function Pure_F   (Self : T) return Integer
>>      with Pure;
>>   function Impure_F (Self : T) return Integer;
>> private
>>   type T is tagged record
>>      I : Integer := 0;
>>   end record;
>> end P;
>>
>>
>> Functions with a Pure contract would be allowed to call other
>> functions with pure contracts, read values/parameters but promise to
>> change nothing (not even via 'tricks' a la random number generator!!).
> 
> We've argued this for a long time within the ARG, and we haven't been able 
> to get a real consensus. This discussion goes back to Ada 79 (which is even 
> before I got involved in Ada) -- early drafts of Ada had both functions 
> (which were what we now call pure) and value-returning procedures (which 
> were not). The concern was that there was not a clear line between them, and 
> moreover there are many sorts of functions that are "logically" pure but 
> still do change things (the "memo function" being the banner carrier for 
> that idea).

I think that the problem may be resolved by considering the contexts where
the function is pure. There is no absolutely pure functions, any one is
impure because it returns something, pumps stack etc. The result is taken
out of consideration, so are local variables etc. There should be some
syntax for specifying what is not touched at the given level of "purity"
and what is.

A related issue is a requirement that functions impure only in their
results and locals were evaluated at compile time when arguments are
statically known. [Needed for handling dimensioned values and similar
static checks, e.g. matrix dimensions checks etc]

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Pure function aspect?...

[stefan-lucks]

On Thu, 12 Jan 2012, Randy Brukardt wrote:

> "Martin" <martin@thedowies.com> wrote in message 
[...]
> > Functions with a Pure contract would be allowed to call other
> > functions with pure contracts, read values/parameters but promise to
> > change nothing (not even via 'tricks' a la random number generator!!).
>
> I had tried an alternative approach for Ada 2012, by suggesting the addition 
> of checked global in/out contracts to subprograms. Eventually, this was 
> dropped from Ada 2012 as being insufficiently mature. 

Very regrettable! 

But reading the AI makes one understand why this is so complicated. There 
are class-wide-operations. If any pure function (or rather, any 
side-effect-free function or procedure) is going to use them, these need 
their own aspect annotations. Thee are the descendents from 
Ada.Finalization.*. There are instances of generic subprograms. Even if 
the generic subprogram is side-effect-free by itself, the 
side-effect-freeness of the instance is likely to depend on the 
side-effect-freeness of the generic parameters ...

However, another reason, why the AI became so complex, seems to be the 
attempt to rather precisely specify side-effects, instead of providing 
just the ability to declare "no side effects". Now it is too late, but a 
simplified approach, allowing only "with Global in out => null;" with the 
option to extend this later would have been acceptable for Ada 2012. :-/

BTW, why do you write "with Global in out => (null);" with brackets?

> My understanding is 
> that AdaCore is experimenting with a version of it in their formal methods 
> research, so it isn't necessarily gone forever (which is good, considering 
> the amount of time I put in on it). You can see the last proposal at 
> http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0186-1.txt.

-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: Pure function aspect?...

[Martin]

On Jan 13, 12:00 am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> "Martin" <mar...@thedowies.com> wrote in message
>
> news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com...
>
>
>
>
>
>
>
>
>
> > Now Ada has bitten the bullet and allowed "in out" mode parameters in
> > functions, is it time to allow users to contract the other extreme and
> > allow a function to be declared Pure (no state changes, not even
> > hidden ones)? e.g.
>
> > package P is
> >   type T is tagged private;
> >   function Pure_F   (Self : T) return Integer
> >      with Pure;
> >   function Impure_F (Self : T) return Integer;
> > private
> >   type T is tagged record
> >      I : Integer := 0;
> >   end record;
> > end P;
>
> > Functions with a Pure contract would be allowed to call other
> > functions with pure contracts, read values/parameters but promise to
> > change nothing (not even via 'tricks' a la random number generator!!).
>
> We've argued this for a long time within the ARG, and we haven't been able
> to get a real consensus. This discussion goes back to Ada 79 (which is even
> before I got involved in Ada) -- early drafts of Ada had both functions
> (which were what we now call pure) and value-returning procedures (which
> were not). The concern was that there was not a clear line between them, and
> moreover there are many sorts of functions that are "logically" pure but
> still do change things (the "memo function" being the banner carrier for
> that idea).
>
> Personally, I would be happy to have strong checks on such functions, and I
> don't much care about what gets left out (it's not that important, and any
> such functions are not task-safe anyway, so it is already a good idea to
> avoid them in Ada code). But not everyone agrees. We just had another
> version of this discussion in Denver; we ended up adopting an undetectable
> bounded error for this case (in the case of assertions, including
> preconditions, et. al.).
>
> I had tried an alternative approach for Ada 2012, by suggesting the addition
> of checked global in/out contracts to subprograms. Eventually, this was
> dropped from Ada 2012 as being insufficiently mature. My understanding is
> that AdaCore is experimenting with a version of it in their formal methods
> research, so it isn't necessarily gone forever (which is good, considering
> the amount of time I put in on it). You can see the last proposal athttp://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0186-1.txt.
>
>                                                              Randy.


Interesting...to my untrained-in-SPARK eye, it looks a little SPARK-
ish! :-)

How would that work together with "limited with"? I'm thinking of
times when I have mutually dependent packages (hence the limited
withs!) _and_ functions that 'tamper' with objects in the other
package. If you have mutually dependent packages, I would have thought
it was almost guaranteed that each would 'tamper' with the other!

-- Martin


-- Martin

Re: Pure function aspect?...

[Martin]

On Jan 13, 8:45 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Thu, 12 Jan 2012 18:00:05 -0600, Randy Brukardt wrote:
> > "Martin" <mar...@thedowies.com> wrote in message
> >news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com...
> >> Now Ada has bitten the bullet and allowed "in out" mode parameters in
> >> functions, is it time to allow users to contract the other extreme and
> >> allow a function to be declared Pure (no state changes, not even
> >> hidden ones)? e.g.
>
> >> package P is
> >>   type T is tagged private;
> >>   function Pure_F   (Self : T) return Integer
> >>      with Pure;
> >>   function Impure_F (Self : T) return Integer;
> >> private
> >>   type T is tagged record
> >>      I : Integer := 0;
> >>   end record;
> >> end P;
>
> >> Functions with a Pure contract would be allowed to call other
> >> functions with pure contracts, read values/parameters but promise to
> >> change nothing (not even via 'tricks' a la random number generator!!).
>
> > We've argued this for a long time within the ARG, and we haven't been able
> > to get a real consensus. This discussion goes back to Ada 79 (which is even
> > before I got involved in Ada) -- early drafts of Ada had both functions
> > (which were what we now call pure) and value-returning procedures (which
> > were not). The concern was that there was not a clear line between them, and
> > moreover there are many sorts of functions that are "logically" pure but
> > still do change things (the "memo function" being the banner carrier for
> > that idea).
>
> I think that the problem may be resolved by considering the contexts where
> the function is pure. There is no absolutely pure functions, any one is
> impure because it returns something, pumps stack etc. The result is taken
> out of consideration, so are local variables etc. There should be some
> syntax for specifying what is not touched at the given level of "purity"
> and what is.
[snip]


Care to mock up an example of the levels you had in mind?

Is it something like (and stealing Randy's "Global"):


function F1 (P1 : T1; P2 : T2) return Boolean
  with Pure => (Global, P1);  -- promise to not change globals or
parameter P1, might tamper with P2

function F1 (P1 : T1; P2 : T2) return Boolean
  with Pure => (all);  -- promise to not change anything (other than
subprogram local objects)

function F1 (P1 : in out T1) return Boolean
  with Pure => (Global);  -- promise to not change anything other than
subprogram local objects or parameters


A function with no pure aspect might be equivilent of:

function F1 (P1 : T1; P2 : T2) return Boolean
  with Pure => (null);  -- no promise to not change anything local,
global or parameter


-- Martin

Re: Pure function aspect?...

[Dmitry A. Kazakov]

On Fri, 13 Jan 2012 03:01:35 -0800 (PST), Martin wrote:

> On Jan 13, 8:45�am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> On Thu, 12 Jan 2012 18:00:05 -0600, Randy Brukardt wrote:
>>> "Martin" <mar...@thedowies.com> wrote in message
>>>news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com...
>>>> Now Ada has bitten the bullet and allowed "in out" mode parameters in
>>>> functions, is it time to allow users to contract the other extreme and
>>>> allow a function to be declared Pure (no state changes, not even
>>>> hidden ones)? e.g.
>>
>>>> package P is
>>>> � type T is tagged private;
>>>> � function Pure_F � (Self : T) return Integer
>>>> � � �with Pure;
>>>> � function Impure_F (Self : T) return Integer;
>>>> private
>>>> � type T is tagged record
>>>> � � �I : Integer := 0;
>>>> � end record;
>>>> end P;
>>
>>>> Functions with a Pure contract would be allowed to call other
>>>> functions with pure contracts, read values/parameters but promise to
>>>> change nothing (not even via 'tricks' a la random number generator!!).
>>
>>> We've argued this for a long time within the ARG, and we haven't been able
>>> to get a real consensus. This discussion goes back to Ada 79 (which is even
>>> before I got involved in Ada) -- early drafts of Ada had both functions
>>> (which were what we now call pure) and value-returning procedures (which
>>> were not). The concern was that there was not a clear line between them, and
>>> moreover there are many sorts of functions that are "logically" pure but
>>> still do change things (the "memo function" being the banner carrier for
>>> that idea).
>>
>> I think that the problem may be resolved by considering the contexts where
>> the function is pure. There is no absolutely pure functions, any one is
>> impure because it returns something, pumps stack etc. The result is taken
>> out of consideration, so are local variables etc. There should be some
>> syntax for specifying what is not touched at the given level of "purity"
>> and what is.
> [snip]
> 
> Care to mock up an example of the levels you had in mind?
> 
> Is it something like (and stealing Randy's "Global"):

Global = Standard (the topmost Ada package is Standard).

A body is impure in some nested context and pure outside it. So the meaning
is not pure-in-A, but rather pure-outside-A, while impure inside A. E.g.

      with Pure => (out Foo)
          -- Pure outside the specification of Foo, can change parameters

      with Pure => (out body Foo)
          -- Pure outside the body of Foo, cannot change parameters

      with Pure => (in Standard)
          -- Pure everywhere = static, constant

   type Func is not null access function (X : Float) return Float
      with Pure => ...;
   function Integrate (F : Func) return Float
      with Pure => (out Integrate and out Func)
          -- Pure outside the specification of Integrate everwhere
          -- Func is pure as well

> A function with no pure aspect might be equivilent of:
> 
> function F1 (P1 : T1; P2 : T2) return Boolean
>   with Pure => (null);  -- no promise to not change anything local,
> global or parameter

   function F1 ...
      with Pure => (out Standard)
         -- impure, out Standard = empty set = null

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Pure function aspect?...

[Randy Brukardt]

<stefan-lucks@see-the.signature> wrote in message 
news:Pine.LNX.4.64.1201131048370.2287@medsec1.medien.uni-weimar.de...
> On Thu, 12 Jan 2012, Randy Brukardt wrote:
...
> However, another reason, why the AI became so complex, seems to be the
> attempt to rather precisely specify side-effects, instead of providing
> just the ability to declare "no side effects".

There has been strong opposition to a "checked" pure function declaration (I 
had floated that first, and it went nowhere), and global in out => null is 
essentially the same thing. The reason is the "memo function" idea (more 
sensibly, a function that logs its calls but is otherwise pure) is not 
allowed. I was trying to do something broader that could get more support.

And just declaring "no side-effects" without checking it is actively harmful 
in my opinion because, perversely, it makes a program less safe. That's 
because the compiler is going to take advantage of this declaration to 
remove calls (especially in contracts and assertions), and if the call in 
fact has side-effects, doing that is not safe (and can easily lead to bugs 
or even erroneous execution). (And if you aren't going to let the compiler 
take advantage of this knowledge, declaring it is pointless.)

I have some lengthy examples of this problem that are tooo long to present 
here (and at least get any other work done), but trust me, it is very real.

The lack in global in out isn't a deal breaker for Ada 2012, simply because 
it is also missing exception contracts. And we need (at least) both of those 
to have enough completeness to really reason formally about Ada programs. 
Hopefully, future versions of Ada will take up both of these again.

                                          Randy.

Re: Pure function aspect?...

[Martin]

On Jan 14, 12:00 am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> <stefan-lu...@see-the.signature> wrote in message
>
> news:Pine.LNX.4.64.1201131048370.2287@medsec1.medien.uni-weimar.de...
>
> > On Thu, 12 Jan 2012, Randy Brukardt wrote:
> ...
> > However, another reason, why the AI became so complex, seems to be the
> > attempt to rather precisely specify side-effects, instead of providing
> > just the ability to declare "no side effects".
>
> There has been strong opposition to a "checked" pure function declaration (I
> had floated that first, and it went nowhere), and global in out => null is
> essentially the same thing. The reason is the "memo function" idea (more
> sensibly, a function that logs its calls but is otherwise pure) is not
> allowed. I was trying to do something broader that could get more support.

You mean people want a method of saying "these state changing calls
are unimportant"?

with Logger;   -- Perhaps allowing 'limited with' if only needed in
the aspect?
package ... is
   function Foo (P1 : Integer)
      return Integer
      with Pure => all or (Logger.Report (S : String) and
Logger.Report (S : String; I : Integer));
...

I think you'd need to enumerate all 'ignorable' state-changing calls.
Or perhaps a short-hand:

with Logger;   -- Perhaps allowing 'limited with' if only needed in
the aspect?
package ... is
   function Foo (P1 : Integer)
      return Integer
      with Pure => all or (package Logger);
...




> And just declaring "no side-effects" without checking it is actively harmful
> in my opinion because, perversely, it makes a program less safe. That's
> because the compiler is going to take advantage of this declaration to
> remove calls (especially in contracts and assertions), and if the call in
> fact has side-effects, doing that is not safe (and can easily lead to bugs
> or even erroneous execution). (And if you aren't going to let the compiler
> take advantage of this knowledge, declaring it is pointless.)
>
> I have some lengthy examples of this problem that are tooo long to present
> here (and at least get any other work done), but trust me, it is very real.
>
> The lack in global in out isn't a deal breaker for Ada 2012, simply because
> it is also missing exception contracts.

Something like:

   function Foo (P1 : Integer)
      return Integer or raise Program_Error or My_Defined_Error;

? Getting a bit long winded but I guess you just need all that sort of
information.


> And we need (at least) both of those
> to have enough completeness to really reason formally about Ada programs.
> Hopefully, future versions of Ada will take up both of these again.

Yes, please!

-- Martin

Re: Pure function aspect?...

[Randy Brukardt]

"Martin" <martin@thedowies.com> wrote in message 
news:9f0669ff-6cb9-4936-9a05-655867639fed@hs8g2000vbb.googlegroups.com...
On Jan 14, 12:00 am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> <stefan-lu...@see-the.signature> wrote in message
...
>> There has been strong opposition to a "checked" pure function declaration 
>> (I
>> had floated that first, and it went nowhere), and global in out => null 
>> is
>> essentially the same thing. The reason is the "memo function" idea (more
>> sensibly, a function that logs its calls but is otherwise pure) is not
>> allowed. I was trying to do something broader that could get more 
>> support.
>
>You mean people want a method of saying "these state changing calls
>are unimportant"?

Something on that line. The global in/out proposal handling that in terms of 
allowing the specification of what state is modified. If that state doesn't 
conflict with other routines, then optimization is still possible.

But one of the important points is that side-effects really ought to prevent 
optimization (and assumptions) unless the compiler (or proof tool) can 
actually prove they don't matter. A call that is being logged, for instance, 
probably shouldn't be eliminated even if the results are the same (because 
you couldn't easily relate the actual calls to the source code).

One can argue the other side of this, too, and it's obvious there are no 
easy answers. In which case I prefer to stay as close to the "canonical" 
semantics as possible.

...
>> The lack in global in out isn't a deal breaker for Ada 2012, simply 
>> because
>> it is also missing exception contracts.
>
>Something like:
>
>  function Foo (P1 : Integer)
>      return Integer or raise Program_Error or My_Defined_Error;
>
>? Getting a bit long winded but I guess you just need all that sort of
>information.

Well, clearly it would be an aspect (like the other contracts), and each 
exception ought to be able to have an optional postcondition as well (which 
defines when the exception might be raised). So more like:

   function Foo (P1 : Integer) return Integer
      when Pre => ...
               Post => ...
               Raises => Program_Error, Storage_Error,
                                My_Defined_Error when P1 not in Even,
               Global in => null,
               Global out => null;

The exception contract would require that the compiler prove that 
Constraint_Error and Tasking_Error are not propagated. (The same would  be 
true for Storage_Error, but that would be impossible for the vast majority 
of compilers). I'm also proposing a way to name a group of exceptions, so 
you wouldn't have to write huge sets repeatedly. (All of the exceptions in 
package IO_Exceptions could be named "IO_Exceptions" so it wouldn't be 
necessary to write about them individually.)

I of course have no idea how far any of this will get, it won't be taken up 
for a while and won't be standardized for years, and in any case, it is all 
optional. No one is going to be required to have complete contracts (I 
suspect that will be going too far).

                                            Randy.

Re: Pure function aspect?...

[Dmitry A. Kazakov]

On Wed, 18 Jan 2012 19:17:45 -0600, Randy Brukardt wrote:

> "Martin" <martin@thedowies.com> wrote in message 

>>> The lack in global in out isn't a deal breaker for Ada 2012, simply 
>>> because
>>> it is also missing exception contracts.
>>
>>Something like:
>>
>>  function Foo (P1 : Integer)
>>      return Integer or raise Program_Error or My_Defined_Error;
>>
>>? Getting a bit long winded but I guess you just need all that sort of
>>information.
> 
> Well, clearly it would be an aspect (like the other contracts), and each 
> exception ought to be able to have an optional postcondition as well (which 
> defines when the exception might be raised). So more like:
> 
>    function Foo (P1 : Integer) return Integer
>       when Pre => ...
>                Post => ...
>                Raises => Program_Error, Storage_Error,
>                                 My_Defined_Error when P1 not in Even,

The problem here is that the exception contracts do not obey the law of
excluded middle. I.e. raise A or not raise A is not necessarily true. The
syntax should distinguish promises (not to raise A) with obligations (to
raise A). In the above you have a negated promise not raise Program_Error,
i.e. Foo *may* raise Program_Error, but it is not required to do so. On the
contrary, My_Defined_Error is an obligation, Foo is *required* to raise it
when the condition is not met.

This is "intuitionistic logic," a bit complicated thing, but necessary
here. The simplest way to handle it would be to have:

function Foo ...
   <a-nice-name-for-possible-exceptions> => X,
   <necessary-exceptions> => Y

Y is a subset of X. Foo never raises anything from not X.

Inference of contracts of possible exceptions is simple. A conservative
estimation is a union of all exception sets of called subprograms for which
no handler is present.

For necessary exceptions it is in general impossible to do (equivalent to
halting). So it looks more appropriate for SPAK than for Ada.

>                Global in => null,
>                Global out => null;
> 
> The exception contract would require that the compiler prove that 
> Constraint_Error and Tasking_Error are not propagated. (The same would  be 
> true for Storage_Error, but that would be impossible for the vast majority 
> of compilers).

Storage_Error should be a conditional:

   may_raise Storage_Error when Standard_Pool'Free_Space < 1024;

Actually any exception should be. E.g.

   procedure Sort (X : in out Data; F : Order_Func)
      may_raise Program_Error when Order_Func may_raise Program_Error;
         -- Sort does not raise Program_Error by itself

> I'm also proposing a way to name a group of exceptions, so 
> you wouldn't have to write huge sets repeatedly. (All of the exceptions in 
> package IO_Exceptions could be named "IO_Exceptions" so it wouldn't be 
> necessary to write about them individually.)

It is time to make exception a proper discrete type with another type for
sets of exceptions. It would be nice to have a tree order of exceptions,
i.e. extensible sets of exceptions too.
 
> I of course have no idea how far any of this will get, it won't be taken up 
> for a while and won't be standardized for years, and in any case, it is all 
> optional. No one is going to be required to have complete contracts (I 
> suspect that will be going too far).

No need to have complete contracts because there is a gray area between
'may raise' and 'must raise'.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de