RE: [rohc] Updated FN Draft - Appendix A

["Lars-Erik Jonsson \(LU/EAB\)" <lars-erik.jonsson at ericsson.com>]

> On Mar 30 2005, at 13:46 Uhr, Lars-Erik Jonsson ((LU/EAB)) wrote:
> 
> > I had preferred a let statement that was only used for the
> > purpose of making definitions, while having a separate mechanism
> > for assertions.
> 
> The problem here is that we don't seem to be communicating very well 
> between the different mindsets.

Agree!

> Given that I'm looking at FN from a relational mindset, I'm still not 
> sure what the distinction is.

So, let's look at the examples you've given...


> Example 1:
> 
> variable_length_32_enc(flag) ===
> {
>          uc_format = field; %[ 32 ]
> 
>          co_format_not_present = field, %[ 0 ]
>          {
>             let(flag == 0);
>             field ::= static;
>          };
>          co_format_8_bit = field, %[ 8 ]
>          {
>             let(flag == 1);
>             field ::= lsb(8, 63);
>          };
>          co_format_16_bit = field, %[ 16 ]
>          {
>             let(flag == 2);
>             field ::= lsb(16, 16383);
>          };
>          co_format_32_bit = field, %[ 32 ]
>          {
>             let(flag == 3);
>             field ::= irregular(32);
>          };
> };

This is what I call a typical assertion, in non-matematical
English I would express this as an "If"-condition.
 
> Example 2:
> 
> irreg_tos_tc ===
> {
>          uc_format = tos_tc; %[ 6 ]
> 
>          co_format_tos_tc_present = tos_tc, %[ 6 ]
>          {
>             let(ecn_used:uncomp_value == 1);
>             tos_tc  ::= irregular (6);
>          };
> 
>          co_format_tos_tc_not_present = tos_tc, %[ 0 ]
>          {
>             let(ecn_used:uncomp_value == 0);
>             tos_tc  ::= static;
>          };
> };

This is what I call a typical assertion, in non-matematical
English I would express this as an "If"-condition.

 
> Example 3:
> [...]
>          co_format_ipv6_innermost_irregular =
>          {
>                  let(ip_inner_ecn:uncomp_value ==
>                      ip_ecn_flags:uncomp_value);
>          };
> [...]

I'm not sure about the context here! I guess this is also an "if".


> Example 4:
> [...]
>          co_format_eol_irregular =
>          {
>                  let(nbits - 8 == pad_len:uncomp_value);
>          };
> [...]

I'm not sure about the context here! I guess this is also an "if".

 
> Example 5:
> [...]
>          co_format_sack1_list_item = discriminator,
>                                      block_1,
>          {
>                  let(length:uncomp_value == 10);
>                  discriminator ::= '00000001';
>                  block_1 ::= tcp_opt_sack_block (ack_value);
>          };
> [...]

This also seems to be what I call a typical assertion, in
non-matematical English I would express this as an "If"-condition.

 
> Example 6:
> [...]
>        let (seq_number_scaled:uncomp_value ==
>                 seq_number:uncomp_value / payload_size);
>        let (seq_number_residue:uncomp_value ==
>                 mod(seq_number:uncomp_value, payload_size));
>        let (ack_number:uncomp_value ==
>                 (ack_stride:uncomp_value * 
> ack_number_scaled:uncomp_value) +
>                 ack_number_residue:uncomp_value);
>        let (ack_number_residue:uncomp_value ==
>                 mod(ack_number:uncomp_value, 
> ack_stride:uncomp_value));
> [...]

This is what I call a definition, also what I believe is
the intuitive meaning of let. This usage of let is what is
exemplified in appendix B. To me, let can never be false,
while a condition (assertion, "if") of course can, as that
is the purpose of it.

/L-E

_______________________________________________
Rohc mailing list
Rohc at ietf.org
https://www1.ietf.org/mailman/listinfo/rohc