archives

Predicate calculus in program verification

Predicate calculus is an indispensable tool for program verification. Therefore any program verifier has to be able to reason with quantified expressions, i.e. universally and existentially quantified expressions.

The proof engine of Modern Eiffel is able to perform such reasoning. The following article
"Quantified Expressions and Predicate Calculus" describes the way in which Modern Eiffel's proof engine handles quantified expressions.

The previous articles Introduction to the proof engine and Proofs by contradiction illustrate the basics of the proof engine.

Pythonect 0.1.0 Release

Hi All,

I'm pleased to announce the first beta release of Pythonect interpreter.

Pythonect is a new, experimental, general-purpose dataflow programming language based on Python.

It aims to combine the intuitive feel of shell scripting (and all of its perks like implicit parallelism) with the flexibility and agility of Python.

Pythonect interpreter (and reference implementation) is written in Python, and is available under the BSD license.

Here's a quick tour of Pythonect:

The canonical "Hello, world" example program in Pythonect:

>>> "Hello World" -> print
<MainProcess:Thread-1> : Hello World
Hello World
>>>

'->' and '|' are both Pythonect operators.

The pipe operator (i.e. '|') passes one item at a item, while the other operator passes all items at once.

Python statements and other None-returning function are acting as a pass-through:

>>> "Hello World" -> print -> print
<MainProcess:Thread-2> : Hello World
<MainProcess:Thread-2> : Hello World
Hello World
>>>

>>> 1 -> import math -> math.log
0.0
>>>

Parallelization in Pythonect:

>>> "Hello World" -> [ print , print ]
<MainProcess:Thread-4> : Hello World
<MainProcess:Thread-5> : Hello World
['Hello World', 'Hello World']

>>> range(0,3) -> import math -> math.sqrt
[0.0, 1.0, 1.4142135623730951]
>>>

In the future, I am planning on adding support for multi-processing, and even distributed computing.

The '_' identifier allow access to current item:

>>> "Hello World" -> [ print , print ] -> _ + " and Python"
<MainProcess:Thread-7> : Hello World
<MainProcess:Thread-8> : Hello World
['Hello World and Python', 'Hello World and Python']
>>>

>>> [ 1 , 2 ] -> _**_
[1, 4]
>>>

True/False return values as filters:

>>> "Hello World" -> _ == "Hello World" -> print
<MainProcess:Thread-9> : Hello World
>>>

>>> "Hello World" -> _ == "Hello World1" -> print
False
>>>

>>> range(1,10) -> _ % 2 == 0
[2, 4, 6, 8]
>>>

Last but not least, I have also added extra syntax for making remote procedure call easy:

>>> 1 -> inc@xmlrpc://localhost:8000 -> print
<MainProcess:Thread-2> : 2
2
>>>

Download Pythonect v0.1.0 from: http://github.com/downloads/ikotler/pythonect/Pythonect-0.1.0.tar.gz

More information can be found at: http://www.pythonect.org

I will appreciate any input / feedback that you can give me.

Thanks,

Itzik Kotler