Hello everyone.

I am a student working on network protocols. Now I have a rough idea
to use mathematical tools, e.g. formal methods, to examine or even
build the model of protocols.

As I have no in-depth concept of these tools, I would like now ask
some naive questions:

1. What is the relationship between formal methods and type theory, as
some papers mentioned that they are inter-related.

2. What is lamda calculus and its relationship with formal methods.

Any help will be appreciated. Thanks very much!

Ed

And here are some naive answers.

1. Type checking proves properties about the code. The compiler proves your assertion that your function returns an int, or that it returns something whose type depends on the types of the arguments in some way. They can also prove other claims you make about your functions, like whether they throw any exceptions (which Java supports) or what side effects the functions may have (which Haskell supports, albeit without any granularity). Regarding network I/O, searching for things like "monad", "linear types", "uniqueness types", and maybe "session types" might reveal some more information.

2. You can read about lambda calculus on Wikipedia, and I don't know its relationship to formal methods.

Try this link
Maybe some freeware from there site can be helpfull for you.

Nice

That's very nice of you two. Thank you very much!

As far as Lambda Calclus is concerned it is a mathematical way
to write computer programs and that too recursive programms.

To give u a taste ::

let y = lambda

y:f(x)->x+1

this is a lambda statement that says f is a function that takes an argument and add 1 to it

Lambda calclus can be seen in pure Type strong languages like Gofer.

Formal mathods is used for programme specification..
When u are building a software It needs

1: Specification
2: Design
3: code
4:test
5:maintain

In specifications we specify the problems in terms of functional parameters....

Tell me If that hepls.

y:f(x)->x+1 is, um "nonstandard" notation. (Meaning: Where the heck did you come up with that?)

The lambda calculus notation for a function such as that would be
\x.x+1
where \ is meant to be the lambda character (but I don't have a unicode keyboard handy).