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!


8 Years
Discussion Span
Last Post by shrughes

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 :)

Votes + Comments
Maybe not.

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


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

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

Tell me If that hepls.

Votes + Comments
This notation is complete nonsense.

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
where \ is meant to be the lambda character (but I don't have a unicode keyboard handy).

This question has already been answered. Start a new discussion instead.
Have something to contribute to this discussion? Please be thoughtful, detailed and courteous, and be sure to adhere to our posting rules.