# HHLPy
HHLPy is a formal verification tool for hybrid systems. It is based on an
extension of Hoare logic to hybrid systems called Hybrid Hoare Logic.
## Installation
### Base installation
The base installation of HHLPy does not require Wolfram Engine:
* Install Python 3.9 or higher: https://www.python.org/downloads/.
* Run `pip install hhlpy` or `python -m pip install hhlpy` to install HHLPy.
* Run `python -m hhlpy` to start HHLPy. Your browser should open automatically.
(If it doesn't, open `http://127.0.0.1:8000/` in your browser.)
### Install Wolfram Engine
To be able to proof more verification conditions, install Wolfram Engine on your system:
* Download Wolfram Engine and install it: https://www.wolfram.com/engine/
* Get a license for Wolfram Engine and activate it.
* If you use the standard installation path, HHLPy should be able to
find it automatically; simply run `python -m hhlpy`.
* If you see the message `Please install Wolfram Kernel ...`, you
need to set the environment variable `WolframKernel` to the path of the file
`WolframKernel` or `WolframKernel.exe` that comes with the Wolfram Engine
installation. Then restart your terminal and run `python -m hhlpy`.
* If you see the line `Socket exception: Socket operation aborted.` in the terminal,
you probably still need to activate your license.
## First Steps
Click on the file `basic1.hhl` in the list of example files on the left panel. A
file with the following content will open:
```
pre [x >= 0];
x := x+1;
post [x >= 1];
```
This example program has a single instruction: it increases the variable x by 1.
The only precondition is `x >= 0`; the only postcondition is `x >= 1`.
These conditions seem correct: If `x` is at least `0` and increased by `1`, it
is at least `1` afterwards.
On the right side, you see the verification condition panel. It contains a
single verification condition that has been generated from the program:
```
assume:
x >= 0
show: x + 1 >= 1
```
Click on the button `Verify` to check the verification condition. A green
checkmark appears below the condition. And the counter next to the button
indicates that `1/1` verification conditions have been proved.
Next, add a second instruction to the program that divides x by 2:
```
pre [x >= 0];
x := x+1;
x := x/2;
post [x >= 1];
```
Observe that the verification condition on the right updates automatically.
Click the button `Verify` to verify the new condition. You will see an X mark
indicating that the verification condition could not be verified. Try to adapt
the postcondition to make the verification go through...
Explore the other example files to see more!
Raw data
{
"_id": null,
"home_page": "",
"name": "hhlpy",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.9",
"maintainer_email": "",
"keywords": "hhl,hybrid systems,hoare logic",
"author": "Huanhuan Sheng, Bohua Zhan, Alexander Bentkamp",
"author_email": "",
"download_url": "https://files.pythonhosted.org/packages/2e/be/c7ac3820b077ea3ab7120c88f070a16b17f3a0f4ed9b3ea2b4b39c1daf7d/hhlpy-0.1.0.tar.gz",
"platform": null,
"description": "# HHLPy\n\nHHLPy is a formal verification tool for hybrid systems. It is based on an\nextension of Hoare logic to hybrid systems called Hybrid Hoare Logic.\n\n## Installation\n\n### Base installation\n\nThe base installation of HHLPy does not require Wolfram Engine:\n* Install Python 3.9 or higher: https://www.python.org/downloads/.\n* Run `pip install hhlpy` or `python -m pip install hhlpy` to install HHLPy.\n* Run `python -m hhlpy` to start HHLPy. Your browser should open automatically.\n (If it doesn't, open `http://127.0.0.1:8000/` in your browser.)\n\n### Install Wolfram Engine\n\nTo be able to proof more verification conditions, install Wolfram Engine on your system:\n* Download Wolfram Engine and install it: https://www.wolfram.com/engine/\n* Get a license for Wolfram Engine and activate it.\n* If you use the standard installation path, HHLPy should be able to\nfind it automatically; simply run `python -m hhlpy`.\n* If you see the message `Please install Wolfram Kernel ...`, you\nneed to set the environment variable `WolframKernel` to the path of the file\n`WolframKernel` or `WolframKernel.exe` that comes with the Wolfram Engine\ninstallation. Then restart your terminal and run `python -m hhlpy`.\n* If you see the line `Socket exception: Socket operation aborted.` in the terminal,\nyou probably still need to activate your license. \n\n## First Steps\n\nClick on the file `basic1.hhl` in the list of example files on the left panel. A\nfile with the following content will open:\n```\npre [x >= 0];\nx := x+1;\npost [x >= 1];\n```\nThis example program has a single instruction: it increases the variable x by 1.\nThe only precondition is `x >= 0`; the only postcondition is `x >= 1`.\nThese conditions seem correct: If `x` is at least `0` and increased by `1`, it\nis at least `1` afterwards.\n\nOn the right side, you see the verification condition panel. It contains a\nsingle verification condition that has been generated from the program:\n```\nassume:\n x >= 0\nshow: x + 1 >= 1\n```\nClick on the button `Verify` to check the verification condition. A green\ncheckmark appears below the condition. And the counter next to the button\nindicates that `1/1` verification conditions have been proved.\n\nNext, add a second instruction to the program that divides x by 2:\n```\npre [x >= 0];\nx := x+1;\nx := x/2;\npost [x >= 1];\n```\nObserve that the verification condition on the right updates automatically.\nClick the button `Verify` to verify the new condition. You will see an X mark\nindicating that the verification condition could not be verified. Try to adapt\nthe postcondition to make the verification go through...\n\nExplore the other example files to see more!\n",
"bugtrack_url": null,
"license": "",
"summary": "Prove hybrid programs correct using Hybrid Hoare Logic",
"version": "0.1.0",
"split_keywords": [
"hhl",
"hybrid systems",
"hoare logic"
],
"urls": [
{
"comment_text": "",
"digests": {
"md5": "bf6b157c598473c5941b13ebc4a8274f",
"sha256": "9899f4b9084d51525e06ea10d014e08fd87929122f8f2cbf280de557732dcb37"
},
"downloads": -1,
"filename": "hhlpy-0.1.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "bf6b157c598473c5941b13ebc4a8274f",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.9",
"size": 2383740,
"upload_time": "2022-12-12T09:35:25",
"upload_time_iso_8601": "2022-12-12T09:35:25.098323Z",
"url": "https://files.pythonhosted.org/packages/97/24/854e1648d3602dc5d7bac85ad663cca6b8ec22a8092e5ac1ab6dd9bee0ce/hhlpy-0.1.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"md5": "0f4aedb0afd230f55775fe001550ccd4",
"sha256": "a2d93df566fae1d5651963f2fcadd705e6c6b1308bb5526b34d390b883081dfe"
},
"downloads": -1,
"filename": "hhlpy-0.1.0.tar.gz",
"has_sig": false,
"md5_digest": "0f4aedb0afd230f55775fe001550ccd4",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.9",
"size": 2276968,
"upload_time": "2022-12-12T09:35:27",
"upload_time_iso_8601": "2022-12-12T09:35:27.241568Z",
"url": "https://files.pythonhosted.org/packages/2e/be/c7ac3820b077ea3ab7120c88f070a16b17f3a0f4ed9b3ea2b4b39c1daf7d/hhlpy-0.1.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2022-12-12 09:35:27",
"github": false,
"gitlab": false,
"bitbucket": false,
"lcname": "hhlpy"
}
JSON