I'm reading the module prepost, and there are a few issues I would
like to raise.
Disclaimer: I have never programmed in Stratego, the code is most
certainly wrong.
1. The complete file
====================
For reference.
imports
liblib
ContractC
strategies
SearchFunDecl = alltd({
?|InitDeclarator[ ~Declarator: <id>~ ]| ; debug
; oncetd(?|DirectDeclarator[ ~ID: fun_name~ ]|)
; oncetd(
?|DirectDeclarator[
DirectDeclarator(ParameterTypeList)
PreCondition-opt
PostCondition-opt ]|
; !PreCondition-opt
; if ?|PreCondition?[ ]| then
!|Statement[ ; ]| => pre
else
?|PreCondition?[
precondition { ~Assertion+: pre~ } ]|
end
; !PostCondition-opt
; if ?|PostCondition?[ ]| then
!|Statement[ ; ]| => post
; !|ReturnValueDeclaration?[ ]| => ret
else
?|PostCondition?[
postcondition ~ReturnValueDeclaration?: ret~
{ ~Assertion+: post~ } ]|
end
; !|DirectDeclarator[
DirectDeclarator(ParameterTypeList) ]|)
; rules (PrePost : fun_name -> (pre, ret, post))
})
SearchFunDef = alltd({
?|ExternalDeclaration[ ~FunctionDefinition: <id> ~ ]|
; oncetd(?|DirectDeclarator[ ~ID: fun_name ~ ]|
; where(<PrePost> fun_name => (pre, ret, post))
; oncetd(?|BlockItemList[ BlockItem-iter ]|
; !|BlockItemList[ ~BlockItem+:
<concat> [
[|BlockItem[ ~CompoundStatement: pre ~ ]|,
|BlockItem[ ~CompoundStatement: post ~ ]|],
BlockItem-iter
]~]|
))
})
prepost = io-wrap(SearchFunDecl ; SearchFunDef)
2. The strategies
=================
First of all, why the heck should the alltd be in the rules? And BTW,
why the rules are strategies here? As a first improvement, I propose
to move the alltd down to the prepost strategy.
prepost = io-wrap(alltd (FunDecl) ; alltd (FunDef))
Then you see that there are two alltd. Although this allows to have
declarations after the implementation (which is indeed a feature) it
goes against the spirit of C. Therefore it should read
prepost = io-wrap(alltd (FunDecl ; FunDef))
Also, *save the space*! What is this fashion of starting to implement
immediately after `='?
FunDecl =
{
?|InitDeclarator[ ~Declarator: <id>~ ]| ; debug
; oncetd(?|DirectDeclarator[ ~ID: fun_name~ ]|)
; oncetd(
?|DirectDeclarator[
DirectDeclarator(ParameterTypeList)
PreCondition-opt
PostCondition-opt ]|
; !PreCondition-opt
; if ?|PreCondition?[ ]| then
!|Statement[ ; ]| => pre
else
?|PreCondition?[
precondition { ~Assertion+: pre~ } ]|
end
; !PostCondition-opt
; if ?|PostCondition?[ ]| then
!|Statement[ ; ]| => post
; !|ReturnValueDeclaration?[ ]| => ret
else
?|PostCondition?[
postcondition ~ReturnValueDeclaration?: ret~
{ ~Assertion+: post~ } ]|
end
; !|DirectDeclarator[
DirectDeclarator(ParameterTypeList) ]|)
; rules (PrePost : fun_name -> (pre, ret, post))
}
FunDef =
{
?|ExternalDeclaration[ ~FunctionDefinition: <id> ~ ]|
; oncetd(?|DirectDeclarator[ ~ID: fun_name ~ ]|
; where(<PrePost> fun_name => (pre, ret, post))
; oncetd(?|BlockItemList[ BlockItem-iter ]|
; !|BlockItemList[ ~BlockItem+:
<concat> [
[|BlockItem[ ~CompoundStatement: pre ~ ]|,
|BlockItem[ ~CompoundStatement: post ~ ]|],
BlockItem-iter
]~]|
))
}
3. The rules
============
The rules exist, and that's because they make sense. Why just making
strategies? I know, they are equivalent, but so are for and while
loops, and you do use both.
What is the InitDeclarator that we start by matching? Apparently it
is only for debugging, but that's cluttering the code. What are all
these oncetd doing here? This is *so wrong*: the code is trying to
match various piece instead of just matching what it's looking for.
IMNSHO it should look like:
FunDecl =
? |Declarator[fn (arg*) pre post]|
; rules (PrePost : fn -> (cs1*, i, cs2*))
where <?|[precondition { cs1* }]|> (pre);
<?|[postcondition (i) { cs2* }]|> (post)
Is there a nicer way to match pre*, ret and post*? And we'll see for
the function with either a pre- xor a postcondition later...
The other rule/strategy is also quite not understandable!
What is to be done is to create a dynamic rule *that performs the
replacement*!!! Not some pseudo table, which completely defeats the
whole point of dynamic rules.
We want to write something like:
where
When you put the two together, you have:
FunDecl =
? |Declarator[fn (arg*) pre post]|
; rules (InstallContract :
|FunctionDefinition[fn (arg*) { stm* }] => !|[fn (arg*) { stm'* }]
where <?|[precondition { cs1* }]|> (pre);
<?|[postcondition (i) { cs2* }]|> (post);
<install-contract (cs1*, i, cs2*)> (stm) => stm'*)
And for an experimental start, I propose
install-contract (|cs1*, i, cs2*) =
!|[ { cs1* } ~id { cs2*} ]|
We will see the complications later.
I would like to have detailed answers, and particularly from Jesus.
I'm quite sure my code is wrong, but it is probably close to correct,
my Stratego is far from fluent.
